Haskell中存在量化值列表
我想知道为什么这段代码没有进行类型检查：
{-# LANGUAGE ScopedTypeVariables, Rank2Types, RankNTypes #-}
{-# OPTIONS -fglasgow-exts #-}
module Main where
foo :: [forall a. a]
foo = [1]
ghc抱怨：
Could not deduce (Num a) from the context ()
arising from the literal `1' at exist5.hs:7:7
鉴于：
Prelude> :t 1
1 :: (Num t) => t
Prelude>
似乎（Num t）上下文不能匹配arg的（）上下文。 我不明白的一点是，由于（）比（数字）更普遍，所以后者应该包含前者。 这与Haskell缺少对子类型输入的支持有关吗？
感谢您对此发表任何评论。
你在这里没有使用存在量化。 您正在使用排名N类型。
这里[forall a. a] [forall a. a]意味着每个元素必须具有所有可能的类型（不是任何，每个）。 所以[undefined, undefined]将是该类型的有效列表，基本上就是这样。
为了扩大这一点：如果一个列表有类型[forall a. a] [forall a. a]表示所有元素都有类型forall a. a forall a. a 。 这意味着任何接受任何形式参数的函数都可以将该列表的一个元素作为参数。 如果你放入一个比forall a. a更具体类型的元素，这不再是真的forall a. a forall a. a ，所以你不能。
要获得可以包含任何类型的列表，您需要使用存在性量化来定义自己的列表类型。 像这样：
data MyList = Nil | forall a. Cons a MyList
foo :: MyList
foo = Cons 1 Nil
当然，除非您限制元素类型以至少实例化Show ，否则不能对该类型的列表执行任何操作。
首先，您的示例对于当前的GHC甚至没有那么深，因为您还需要启用ImpredecativeTypes 。 这样做会导致警告，ImpredicativeTypes将在下一个GHC中简化或删除。 所以我们在这里没有很好的领域。 尽管如此，添加适当的Num约束（ foo :: [forall a. Num a => a] ）确实可以让您的示例进行编译。
让我们暂时搁置不确定的类型，并看一个更简单的例子：
data Foo = Foo (forall a. a)
foo = Foo 1
这也不会编译错误Could not deduce (Num a) from the context () 。
为什么？ 那么，类型承诺你会给Foo的构造函数的东西的质量，任何类型的a ，它会产生a 。 唯一满足这一点的是底部。 另一方面，整数字面意味着对于任何类型a Num的类型，它会产生一个a 。 所以这些类型显然是不相容的。 然而，我们可以将这些讨论拉得更远一些，以得到你可能想要的东西：
data Foo = forall a. Foo a
foo = Foo 1
这样编译。 但我们可以用它做什么？ 好吧，让我们试着定义一个提取函数：
unFoo (Foo x) = x
哎呀！ Quantified type variable 'a' escapes 。 所以我们可以定义这一点，但我们不能用它做很多有趣的事情。 如果我们给出了一个类的上下文，那么我们至少可以使用它的一些类的功能。
存在时间和地点的存在，包括没有上下文的时间和地点，但相当少见，特别是当你开始时。 当你最终使用它们时，往往会在GADTs的背景下，GADT是存在类型的超集，但其中存在的方式产生感觉很自然。
因为声明[forall a. a] [forall a. a] （意思是）等同于说：“我有一个列表，如果你（即计算机）选择了一个类型，我保证所述列表的元素将是该类型的。”
编译器正在“称呼你的虚张声势”，这样说来，抱怨道：“我知道'如果你给我一个1 ，它的类型是Num类，但是你说我可以选择任何类型的I想为那个名单。“
基本上，你试图使用通用类型的值，就好像它是通用值的类型。 虽然这些不是同一回事。
链接地址: http://www.djcxy.com/p/43429.html