为什么 GHC Haskell 中没有存在量化的类型变量

Question

有普遍量化的类型变量，也有存在量化的数据类型。然而，尽管人们有时会提供 exists a. Int -> a 形式的伪代码来帮助解释概念，但它似乎并不是一个真正感兴趣的编译器扩展。这只是“添加这个没有太大价值”吗？之类的东西（因为它对我来说确实很有价值），或者是否存在诸如不确定性之类的问题，这使得它真的不可能。

编辑： 我已将 viorior 的答案标记为正确，因为这似乎可能是不包括在内的实际原因。我想添加一些额外的评论，以防万一有人想进一步澄清这一点。

根据 cmets 的要求，我将举例说明为什么我认为这很有用。假设我们有如下数据类型：

data Person a = Person
  { age: Int
  , height: Double
  , weight: Int
  , name: a
  }

所以我们选择参数化而不是a，这是一个命名约定（我知道在这个例子中，为美国的“第一、中间、最后”创建一个带有适当数据构造函数的NamingConvention ADT 可能更有意义，西班牙裔“姓名，父亲姓名，母亲姓名”等。但现在，就这样吧）。

因此，我们看到有几个函数基本上忽略了 Person 参数化的类型。例子是

age :: Person a -> Int
height :: Person a -> Double
weight :: Person a -> Int

在这些之上构建的任何函数都可以类似地忽略a 类型。例如：

atRiskForDiabetes :: Person a -> Bool
atRiskForDiabetes p = age p + weight p > 200
--Clearly, I am not actually a doctor

现在，如果我们有一个异构的人员列表（[exists a. Person a] 类型），我们希望能够将我们的一些函数映射到列表上。当然，也有一些没用的映射方式：

heteroList :: [exists a. Person a]
heteroList = [Person 20 30.0 170 "Bob Jones", Person 50 32.0 140 3451115332]
extractedNames = map name heteroList

在这个例子中，extractedNames 当然没有用，因为它的类型是[exists a. a]。但是，如果我们使用我们的其他功能：

totalWeight :: [exists a. Person a] -> Int
totalWeight = sum . map age

numberAtRisk :: [exists a. Person a] -> Int
numberAtRisk = length . filter id . map atRiskForDiabetes

现在，我们有一些有用的东西可以在异构集合上运行（而且，我们甚至没有涉及类型类）。请注意，我们能够重用现有功能。使用存在数据类型如下：

data SomePerson = forall a. SomePerson (Person a) --fixed, thanks viorior

但是现在，我们如何使用age 和atRiskForDiabetes？我们不能。我认为你必须做这样的事情：

someAge :: SomePerson -> Int
someAge (SomePerson p) = age p

这真的很蹩脚，因为您必须为新类型重写所有组合子。如果您想使用通过多个​​类型变量参数化的数据类型来执行此操作，情况会变得更糟。想象一下：

somewhatHeteroPipeList :: forall a b. [exists c d. Pipe a b c d]

我不会进一步解释这种思路，但请注意，您将重写很多组合子以仅使用存在数据类型来执行此类操作。

话虽如此，我希望我已经给出了一个温和的令人信服的用法，这可能是有用的。如果它看起来没有用（或者如果这个例子看起来太做作了），请随时告诉我。另外，由于我最初是一名程序员并且没有接受过类型理论方面的培训，所以我很难在这里看到如何使用 Skolem 的定理（由 viorior 发布）。如果有人能告诉我如何将它应用到我给出的Person a 示例中，我将不胜感激。谢谢。

Answer 1

没必要。

通过斯科伦定理，我们可以将存在量词转换为具有更高等级类型的全称量词：

(∃b. F(b)) -> Int   <===>  ∀b. (F(b) -> Int)

秩 n+1 的每个存在量化类型都可以编码为秩 n 的普遍量化类型

Answer 2

GHC 中存在量化类型are available，因此问题基于错误假设。