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

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

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

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

但是，第一个不被接受，但第二个工作正常(使用 ExistentialQuantification )。

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

最佳答案

你的理解是不对的。问题的很大一部分是您使用的传统存在量化语法对于不完全熟悉它的人来说非常困惑。因此，我强烈建议您改用 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 扩展名，但这确实不起作用，因此您不应该这样做。如果你想要一个存在量化事物的列表，你需要首先将它们包装在存在数据类型中，或者使用专门的存在列表类型。如果你想要一个普遍量化的东西的列表，你需要先把它们包装起来(可能是新的)。

关于haskell - 为什么 `[1, "a"]::[forall a. Show a => a]` 是不允许的？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/33049458/