为什么`[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数据构造是需要的任何 showable东西的功能键入并生成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]是“impandicative”。我不明白这是什么意思的细节，但松散地说，你在->以外的类型构造函数的参数中插入了forall，这是不允许的。 GHC可能会建议您启用ImpredicativeTypes扩展名，但这确实无法正常工作，所以您不应该这样做。如果你想要一个存在量化的事物列表，你需要首先将它们包装在存在的数据类型中，或者使用专门的存在性列表类型。如果你想要一个普遍量化的事物清单，你需要先把它们包装起来（可能是新形式）。