在 Haskell 中实现多态 λ-calculus/System F 对的 Church 编码
Implement in Haskell the Church encoding of the pair for polymorphic λ-calculus/System F
我想在 Haskell 的多态 lambda 演算中实现 Church encoding of the pair。
在 Peter Selinger's notes on lambda calculus 的第 77 页第 8.3.3 节中，他给出了两种笛卡尔积的构造
A×B = ∀α.(A→B→α)→α
⟨M,N⟩ = Λα.λfA→B→α.fMN
对于另一个来源，在第 54 页，Dider Rémy's notes on lambda calculus 的第 4.2.3 节，他将多态 λ-calculus/System 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。我认为额外的上下文和地点的变化可能会使它更明智。
你写了
Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
只需删除应用程序和抽象中的所有类型参数：
λp:α×β.p (λx:α.λy:β.x)
在 Haskell 中，没有类型注释：
\p -> p (\x y -> x)
首先，你说得对，塞林格和雷米说的是同一件事；不同之处在于 Rémy 正在定义 对构造函数 ⟨–,–⟩，它将 M 和 N（他的 x₁ 和 x₂）及其类型（α₁ 和 α₂）作为参数；他定义的其余部分只是 ⟨M,N⟩ 与 β 和 y 的定义，其中 Selinger 具有 α 和 f。
好吧，考虑到这一点，让我们开始转向投影。首先要注意的是∀、Λ、→ 和λ 之间的关系，以及它们在Haskell 中的等价物。回想一下 ∀ 及其居民 Λ 在 类型 上运行，其中 → 及其居民 λ 在 值 上运行。在 Haskell-land 中，大多数这些对应关系很容易，我们得到以下 table
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 : ∀α.α→α
在系统 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 没有！
所以这是我们 table 中的最后一个单元格：在 Haskell 中，所有 Λ 都是隐含的，甚至没有扩展来制作它们explicit.¹ 它们出现的任何地方，我们都忽略它们，type inference 会自动填充它们。因此，要直接回答您的一个明确问题，您可以使用 Haskell forall 来表示系统 F∀，并使用 nothing 来表示系统 F 类型的 lambda Λ.
所以你将第一个投影的定义定义为（重新格式化）
proj₁ = Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
我们通过忽略所有 Λ 及其应用程序（并省略类型注释²）将其转换为 Haskell，我们得到
proj₁ = \p. p (\x y -> x)
或
proj₁ p = p (\x _ -> x)
我们的系统 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
工作正常。
我想在 Haskell 的多态 lambda 演算中实现 Church encoding of the pair。
在 Peter Selinger's notes on lambda calculus 的第 77 页第 8.3.3 节中，他给出了两种笛卡尔积的构造
A×B = ∀α.(A→B→α)→α
⟨M,N⟩ = Λα.λfA→B→α.fMN
对于另一个来源，在第 54 页，Dider Rémy's notes on lambda calculus 的第 4.2.3 节，他将多态 λ-calculus/System 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。我认为额外的上下文和地点的变化可能会使它更明智。
你写了
Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
只需删除应用程序和抽象中的所有类型参数：
λp:α×β.p (λx:α.λy:β.x)
在 Haskell 中，没有类型注释：
\p -> p (\x y -> x)
首先，你说得对，塞林格和雷米说的是同一件事；不同之处在于 Rémy 正在定义 对构造函数 ⟨–,–⟩，它将 M 和 N（他的 x₁ 和 x₂）及其类型（α₁ 和 α₂）作为参数；他定义的其余部分只是 ⟨M,N⟩ 与 β 和 y 的定义，其中 Selinger 具有 α 和 f。
好吧，考虑到这一点，让我们开始转向投影。首先要注意的是∀、Λ、→ 和λ 之间的关系，以及它们在Haskell 中的等价物。回想一下 ∀ 及其居民 Λ 在 类型 上运行，其中 → 及其居民 λ 在 值 上运行。在 Haskell-land 中，大多数这些对应关系很容易，我们得到以下 table
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 : ∀α.α→α
在系统 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 没有！
所以这是我们 table 中的最后一个单元格：在 Haskell 中，所有 Λ 都是隐含的，甚至没有扩展来制作它们explicit.¹ 它们出现的任何地方，我们都忽略它们，type inference 会自动填充它们。因此，要直接回答您的一个明确问题，您可以使用 Haskell forall 来表示系统 F∀，并使用 nothing 来表示系统 F 类型的 lambda Λ.
所以你将第一个投影的定义定义为（重新格式化）
proj₁ = Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
我们通过忽略所有 Λ 及其应用程序（并省略类型注释²）将其转换为 Haskell，我们得到
proj₁ = \p. p (\x y -> x)
或
proj₁ p = p (\x _ -> x)
我们的系统 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
工作正常。