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

Question

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

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

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

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

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

我认为雷米和塞林格说的一样，只是更冗长。

无论如何，根据维基百科，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 中。我认为额外的背景和 field 的变化可能会使它更明智。

Answer 1

首先，Selinger 和 Rémy 说的是同一件事，这确实是正确的；不同之处在于，Rémy 定义了对构造函数⟨–,–⟩，它将 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 风格的能力能够把 forall s 在我们的类型中的任何地方。为此，我们打开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 ∀，没有任何东西来表示 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 γ. α -> β -> γ) -> α

或者，绑定(bind)α和 β明确的，

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 ;然后，任何类型变量绑定(bind)在显式 forall在期限内。所以第一个例子仍然中断，但是

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

工作正常。