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

Question

有全称量化的类型变量，也有存在量化的数据类型。然而，尽管人们有时会提供伪代码形式的exists a. Int -> a来帮助解释概念，但似乎编译器扩展并没有任何真正感兴趣的地方。这只是一种“增加这个没有太多价值”的事情（因为对我来说似乎很有价值），还是像不可判定性那样存在问题，使其真正不可能。

编辑： 我将viorior的答案标记为正确答案，因为这似乎是没有包括它的实际原因。但是，为了防止有人想要进一步澄清这一点，我想添加一些额外的评论。

根据评论的要求，我将举一个例子，说明为什么我认为这很有用。假设我们有一个如下所示的数据类型：

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

因此，我们选择对a进行参数化，这是一种命名约定（我知道在这个例子中创建一个包含“first,middle,last”等适当数据结构的“NamingConvention”ADT可能更有意义，以适应美国人的惯用法和墨西哥裔的“name,paternal name,maternal name”等，但现在就这样吧）。

因此，有几个函数基本上忽略了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]

我不会进一步解释这个思路，但请注意，如果仅使用存在数据类型来做任何类似此操作，您将需要重写许多组合器。

话虽如此，希望我已经给出了一个稍微有说服力的用例。如果它看起来没有用（或者示例似乎过于人为），请随时告诉我。另外，由于我首先是一个程序员，而没有接受过类型理论方面的培训，所以很难看到如何在这里应用斯科勒定理（如viorior发布的）。如果有人能向我展示如何将其应用于我提供的Person a示例，我将非常感激。谢谢。

- Andrew Thaddeus Martin

---

你能提供一个有用的例子吗？我很好奇在Haskell中是否有一个好的使用案例。也有可能你想要那个功能的原因可以使用另一种技术来解决，但没有具体的东西很难说。 - bheklilr

“Does data Exists t = forall a. Exists (t a) work? In your case you'd write foo :: Exists ((->) Int). We do have existentials in this sense, just bounded by a data constructor.”这句话的意思是：“data Exists t = forall a. Exists (t a) 这个语法结构是否可用？在你的情况下，你会写成 foo :: Exists ((->) Int)。我们确实有这种存在类型，只是被一个数据构造器所限制。” - daniel gratzer

你需要把它包装在一个数据类型中，虽然这有些不方便，但是存在类型并不是很常见。 - augustss

UHC有一个用于编写存在类型的扩展，但您无法对存在类型施加约束，使其几乎无用。 - Carl

谢谢，我已经修复了。 - Andrew Thaddeus Martin

Answer 1

这是不必要的。

根据斯科勒姆定理，我们可以将存在量词转化为更高阶类型的全称量词：

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

对于任意存在量化的 n+1 阶类型，都可以编码为一个 n 阶的全称量化类型。

- viorior

---

那么考虑使用 Int -> (∃b. F(b)) 代替呢？ - chi

@viorior 不是。例如，类型F(Int) -> ∃b. F(b)显然是有解的，但是∀b.(F(Int) -> F(b))不是。 - Alexey Romanov

你可以使用 CPS 转换来实现这个，即 F Int -> (forall b . F b -> r) -> r，也就是 flip ($). - J. Abrahamson

值得注意的是，即使它并不是必要的，它也很方便。真正的权衡是方便性与让类型检查器更加困惑并引入新关键字之间的取舍。 - J. Abrahamson

@viorior 不完全正确。1）应该是“同构于”或“可以编码为”，而不是“是”。2）它同构的类型是通用的，但不是 ∀b.(Int -> F(b))。你可以在 https://dev59.com/TGYr5IYBdhLWcg3wdqCv 的答案中找到正确编码的描述。 - Alexey Romanov

Answer 2

GHC 中存在量化类型 可用，因此这个问题是基于错误的假设而提出的。

- Daniel Wagner

---

可以翻译成：存在量化的数据类型可以使用，但问题实际上询问的是类似于 exists a. Int -> a 中的存在量化类型变量，这种类型变量不可用。请注意不要改变原意，使语言简洁易懂，不提供任何解释或额外信息。 - Tikhon Jelvis

有道理。但是相比存在类型，是否有更喜欢存在类型的原因呢？具体而言，与存在数据类型的构造函数调用/模式匹配相比，使用存在类型需要进行打包/解包操作是否更不方便？ - Dominique Devriese

根据我的主观经验，是的。 - javawizard