haskell - 为什么 `[1, "a"]::[forall a. Show 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扩展名，但这真的不能正常工作，所以你不应该。如果您想要一个存在量化事物的列表，您需要首先将它们包装在存在数据类型中或使用专门的存在列表类型。如果您想要一个普遍量化的事物的列表，您需要先将它们包装起来(可能在新类型中)。