在 Haskell 中实现多态 λ-演算/系统 F 对的 Church 编码

Question

我想在 Haskell 的多态 lambda 演算中实现 Church encoding of the pair。

在第 77 页，Peter Selinger's notes on lambda calculus 的第 8.3.3 节，他给出了两种类型的笛卡尔积的构造

A×B = ∀α.(A→B→α)→α
⟨M,N⟩ = Λα.λf^A→B→α.fMN

对于另一个来源，在第 54 页，Dider Rémy's notes on lambda calculus 的第 4.2.3 节，他将多态 λ-演算/系统 F 中对的 Church 编码定义为

Λα₁.Λα₂.λx₁:α₁.λx₂:α₂.Λβ.λy:α₁→α₂→β。 y x₁ x₂

我认为 Rémy 说的和 Selinger 一样，只是更冗长。

无论如何，根据维基百科，Haskell 的类型系统是基于System F，所以我希望可以直接在 Haskell 中实现这种 Church 编码。我有：

pair :: a->b->(a->b->c)->c
pair x y f = f x y

但我不确定如何进行预测。

Λα.Λβ.λp^α×β.pα(λx^α.λy^β.x)

我是否使用 Haskell forall 作为大写 lambda 类型量词？

这与my previous question 基本相同，但使用的是 Haskell 而不是 Swift。我认为额外的背景和场地的变化可能会使它更明智。

Answer 1

首先，Selinger 和 Rémy 说的是同一件事，这确实是正确的；不同之处在于 Rémy 定义了 pair 构造函数 ⟨–,–⟩，它将 M 和 N（他的 x₁ 和 x₂）及其类型（α₁ 和 α₂）作为参数；他定义的其余部分只是 ⟨M,N⟩ 与 β 和 y 的定义，其中 Selinger 有 α 和 f。

好的，处理完这些，让我们开始向预测移动。首先要注意的是∀、Λ、→和λ之间的关系，以及它们在Haskell中的等价物。回想一下，∀ 及其居民 Λ 对 类型 进行操作，其中 → 及其居民 λ 对 值 进行操作。在 Haskell-land 中，大多数这些对应关系都很容易，我们得到下表

          System F                             Haskell
Terms (e)     :  Types (t)        Terms (e)       ::  Types (t)
────────────────────────────────────────────────────────────────
λx:t₁.(e:t₂)  :  t₁ → t₂          \x::t₁.(e::t₂)  :: t₁ -> t₂
Λα.(e:t)      :  ∀α.t             (e::t)          :: forall α. t

术语级别的条目很简单：→ 变为 ->，λ 变为 \。但是∀和Λ呢？

默认情况下，在 Haskell 中，所有的 ∀ 都是隐式的。每次我们引用类型变量（类型中的小写标识符）时，它都会被隐式地普遍量化。所以像

这样的类型签名

id :: a -> a

对应

id : ∀α.α→α

在 System F 中。我们可以打开语言扩展 ExplicitForAll 并获得明确编写这些内容的能力：

{-# LANGUAGE ExplicitForAll #-}
id :: forall a. a -> a

然而，默认情况下，Haskell 只允许我们将这些量词放在定义的开头；我们希望 System F 风格的能力可以将foralls 放在我们类型中的任何位置。为此，我们打开RankNTypes。事实上，从现在开始，所有的 Haskell 代码都将使用

{-# LANGUAGE RankNTypes, TypeOperators #-}

（另一个扩展允许类型名称是运算符。）

既然我们都知道了，我们可以试着写下×的定义。我将其 Haskell 版本称为 ** 以保持不同（尽管如果我们愿意，我们可以使用 ×）。塞林格的定义是

A×B = ∀α.(A→B→α)→α

所以 Haskell 是

type a ** b = forall α. (a -> b -> α) -> α

正如你所说，创建函数是

pair :: a -> b -> a ** b
pair x y f = f x y

但是我们的 Λ 怎么了？它们存在于 ⟨M,N⟩ 的 System F 定义中，但 pair 没有！

所以这是我们表格中的最后一个单元格：在 Haskell 中，所有 Λ 都是隐式的，甚至没有扩展来使它们显式。¹任何出现它们的地方，我们都忽略它们，并且类型推断会自动填充它们。因此，要直接回答您的一个明确问题，您可以使用 Haskell forall 来表示 System F ∀，并使用 nothing 来表示 System F 类型 lambda Λ。

所以你将第一个投影的定义定义为（重新格式化）

proj₁ = Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)

我们通过忽略所有Λ及其应用程序（并省略类型注释²）将其转换为Haskell，然后我们得到

proj₁ = \p. p (\x y -> x)

或

proj₁ p = p (\x _ -> x)

我们的 System F 版本有这种类型

proj₁：∀α.∀β。 α×β→α

或者，展开

proj₁：∀α.∀β。 (∀γ.α→β→γ)→α

事实上，我们的 Haskell 版本有这种类型

proj₁ :: α ** β -> α

再次扩展为

proj₁ :: (forall γ. α -> β -> γ) -> α

或者，使α 和β 的绑定显式，

proj₁ :: forall α β. (forall γ. α -> β -> γ) -> α

为了完整起见，我们还有

proj₂：∀α.∀β。 α×β → β
proj₂ = Λα.Λβ.λp:α×β.p β (λx:α.λy:β.y)

变成了

proj₂ :: α ** β -> β
proj₂ p = p (\_ y -> y)

在这一点上可能不足为奇:-)

---

¹ 与此相关的是，所有 Λ 都可以在编译时擦除 - 编译的 Haskell 代码中不存在类型信息！

² 我们省略 Λs 的事实意味着类型变量在术语中不受约束。以下是错误：

id :: a -> a
id x = x :: a

因为它被视为我们写的

id :: forall a. a -> a
id x = x :: forall b. b

这当然行不通。为了解决这个问题，我们可以打开语言扩展ScopedTypeVariables；然后，绑定在显式forall 中的任何类型变量都在该术语的范围内。所以第一个例子仍然失败，但是

id :: forall a. a -> a
id x = x :: a

工作正常。

Answer 2

你写的

Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)

只需删除应用程序和抽象中的所有类型参数：

λp:α×β.p (λx:α.λy:β.x)

在 Haskell 中，没有类型注释：

\p -> p (\x y -> x)