haskell - 存在类型的理论基础是什么？

Haskell Wiki很好地解释了如何使用存在类型，但我不太理解它们背后的理论。

考虑这个存在类型的例子:

data S = forall a. Show a => S a      -- (1)

为我们可以转换为String的事物定义类型包装器。 wiki 提到我们真正想要定义的是这样的类型

data S = S (exists a. Show a => a)    -- (2)

即真正的“存在”类型 - 松散地我认为这意味着“数据构造函数 S 接受 Show 实例存在的任何类型，并且包裹它”。事实上，您可能可以按如下方式编写 GADT:

data S where                          -- (3)
    S :: Show a => a -> S

我还没有尝试编译它，但看起来它应该可以工作。对我来说，GADT 显然等同于我们要编写的代码 (2)。

但是，我完全不明白为什么 (1) 等于 (2)。为什么将数据构造函数移到外部会将 forall 变成 exists？

我能想到的最接近的是De Morgan's Laws在逻辑中，交换否定和量词的顺序会将存在量词变成全称量词，反之亦然:

¬(∀x. px) ⇔ ∃x. ¬(px)

但是数据构造函数似乎与否定运算符完全不同。

使用 forall 而不是不存在的 exists 定义存在类型的能力背后的理论是什么？

最佳答案

首先，看一下“库里·霍华德对应表”，其中指出计算机程序中的类型对应于直觉逻辑中的公式。直觉逻辑就像你在学校学到的“常规”逻辑一样，但没有排除中间或双重否定消除法则:

逻辑定律

您对德摩根定律的理解是正确的，但首先我们将使用它们来推导出一些新的定律。德摩根定律的相关版本是:

我们可以推导出 (∀x.P ⇒ Q(x)) = P ⇒ (∀x.Q(x)):

并且 (∀x.Q(x) ⇒ P) = (∃x.Q(x)) ⇒ P (下面使用这个):

请注意，这些定律在直觉逻辑中也成立。下面的论文引用了我们推导出的两条定律。

最简单的类型很容易使用。例如:

data T = Con Int | Nil

构造函数和访问器具有以下类型签名:

Con :: Int -> T
Nil :: T

unCon :: T -> Int
unCon (Con x) = x

现在让我们来处理类型构造函数。采用以下数据定义:

data T a = Con a | Nil

这会创建两个构造函数，

Con :: a -> T a
Nil :: T a

当然，在 Haskell 中，类型变量是隐式通用量化的，所以这些实际上是:

Con :: ∀a. a -> T a
Nil :: ∀a. T a

访问器也同样简单:

unCon :: ∀a. T a -> a
unCon (Con x) = x

让我们将存在量词 ∃ 添加到我们的原始类型(第一个类型，没有类型构造函数)。与其将其引入到类型定义中(这看起来不像逻辑)，不如将其引入到构造函数/访问器定义中(这看起来确实像逻辑)。我们稍后将修复数据定义以匹配。

而不是 Int ，我们现在将使用 ∃x. t 。在这里，t是某种类型表达式。

Con :: (∃x. t) -> T
unCon :: T -> (∃x. t)

根据逻辑规则(上面第二条规则)，我们可以重写 Con 的类型至:

Con :: ∀x. t -> T

当我们将存在量词移到外部(prenex形式)时，它就变成了全称量词。

因此，以下内容在理论上是等效的:

data T = Con (exists x. t) | Nil
data T = forall x. Con t | Nil

除了 exists 没有语法在 haskell 。

在非直觉逻辑中，允许从 unCon 的类型导出以下内容: :

unCon :: ∃ T -> t -- invalid!

这是无效的，因为这种转换在直觉逻辑中是不允许的。所以不可能写unCon的类型没有exists关键字，并且不可能将类型签名放在 prenex 形式中。很难让类型检查器保证在这种情况下终止，这就是 Haskell 不支持任意存在量词的原因。

“具有类型推断的一流多态性”，Mark P. Jones，第 24 届 ACM SIGPLAN-SIGACT 编程语言原理研讨会论文集 ( web )

关于haskell - 存在类型的理论基础是什么？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/10753073/