为什么`[1,"a"] :: [forall a.显示a => a]`是不允许的？

Question

在我(可能不正确)的理解中,以下两个列表应该是等效的:

[1, "a"] :: [forall a. Show a => a]

data V = forall a. Show a => V a
[V 1, V "a"] :: [V]

但是,第一个不被接受,但第二个工作正常(有ExistentialQuantification).

如果第一个列表不存在,那么空白中的类型是map V :: ??? -> [V]什么？什么类型的机制强制存在包装器？

Answer 1

你的理解是不对的.问题的一个很大一部分是你使用的传统存在量化语法对于那些不熟悉它的人来说非常困惑.因此,我强烈建议您使用GADT语法,这样做的好处还在于更强大.简单的事情就是启用{-# LANGUAGE GADTs #-}.当我们接触它时,让我们开启{-# LANGUAGE ScopedTypeVariables #-},因为我讨厌想知道forall在任何给定的地方有什么意义.你的V定义与完全相同

data V where
  V :: forall a . Show a => a -> V

forall如果我们愿意,我们实际上可以放弃显式:

data V where
  V :: Show a => a -> V

所以V数据构造函数是一个函数,它接受任何可显示类型的东西并产生类型的东西V.类型map非常严格:

map :: (a -> b) -> [a] -> [b]

传递的列表的所有元素map必须具有相同的类型.所以类型map V就是

map V :: Show a => [a] -> [V]

让我们现在回到你的第一个表达:

[1, "a"] :: [forall a. Show a => a]

现在实际上说的[1, "a"]是一个列表,其中每个元素都有类型forall a . Show a => a.也就是说,如果我提供任何a实例Show,则列表的每个元素都应具有该类型.这是不正确的."a"例如,不具有类型Bool.这里还有另一个问题; 类型[forall a . Show a => a]是"不可预测的".我不明白这意味着什么的细节,但是松散地说你已经陷入forall了类型构造函数的参数而不是->,而且这是不允许的.GHC可能会建议您启用ImpredicativeTypes扩展,但这真的不行,所以你不应该.如果需要存在量化事物的列表,则需要首先将它们包含在存在数据类型中或使用专门的存在列表类型.如果你想要一个普遍量化的东西列表,你需要先将它们包装起来(可能是新类型).