在Haskell中实现多态λ演算/系统F对的教会编码 [英] Implement in Haskell the Church encoding of the pair for polymorphic λ-calculus/System F

问题描述

我想在多态lambda演算中实现对的教会编码 Haskell。

在第77页8.3.3节彼得塞林格关于lambda微积分的笔记，他给出了两种类型的笛卡尔乘积的构造：
$ b A×B =∀α。（A→B→α）→α
⟨M，N⟩=Λα.λfA→B→α.fMN

另一个来源，在第54页， DiderRémy关于lambda微积分的笔记，他将多态λ-演算/系统F中的对的Church编码定义为

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

我认为雷米与塞林格的说法是一样的，只是更加详细地说。

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

  pair :: a-> b->（a-> b-> c ） - > c 
 pair xyf = fxy 
  

但我不确定如何做预测。

Λα.Λβ.λpααββ（λxαββββββ sup> .x）

对于大写lambda类型量词是否使用Haskell forall ？

这基本上与我的上一个问题，但在Haskell而不是Swift中。我认为额外的环境和场地的变化可能会使它更加明智。

首先，你的确是对的塞林格和雷米说同样的话;不同之处在于，雷米正在定义 pair构造函数⟨ - ， - which，其参数M和N（他的x 1和x 2）以及它们的类型（α1和α2）;他的定义的其余部分只是β和y的定义，β和y，其中Selinger有α和f。

好了，照顾好了，让我们开始移动towrads预测。首先要注意的是，∀，Λ，→和λ之间的关系，以及它们在Haskell中的等价关系。回想一下，∀及其居民Λ在类型上操作，其中→和其居民λ在值上操作。在Haskell-land中，大多数这种通信很容易，我们得到下面的表格：

  System F Haskell 
条款（e）：类型（t）条款（e）::类型（t）
──────────────────────────── ─────────────────────────────────────
λx：t 1（e：t 2） ：t 1→t 2 \ x :: t 1（e :: t 2）:: t 1→> t 2 
Λα。（e：t）：∀α.t（e :: t）:: forallα。 t 
  

术语级别条目很简单：→变成 - > 和λ变成 \ 。但是∀和Λ怎么样？

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

  id :: a  - > a 
  

对应于

id：∀系统F中的α.α→α

。我们可以打开语言扩展 ExplicitForAll 并获得明确写出：

  { - ＃LANGUAGE ExplicitForAll＃ - } 
 id :: forall a。 a  - > a 
  

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

$ p $ {$＃$ c $ { - ＃LANGUAGE RankNTypes，TypeOperators＃ - }

（其他扩展名允许类型名称为运算符。）

现在我们知道了所有这些，我们可以尝试写下×的定义。我将调用它的Haskell版本 ** 来区分事情（尽管我们可以使用×）。塞林格的定义是：b
$ b A×B =∀α。（A→B→α）→α

Haskell是

 键入a ** b = forallα。 （a  - > b  - >α） - > α
  

正如您所说，创建函数是

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

但是我们的Λs发生了什么？他们在系统F的定义中，⟨M，N⟩，但 pair 没有！

<所以这是我们表格中的最后一个单元格：在Haskell中，所有的都是隐式的，甚至没有扩展名使它们变得明确。无论它们出现在哪里，我们都忽略它们，和类型推断自动填充它们。因此，要直接回答你的一个明确问题，你可以使用Haskell forall 来表示System F∀，而 nothing 来表示系统F类型lambda∧。

所以你给出了第一个投影的定义（重新格式化）

proj 1 =Λα .λβ：λp：α×β.pα（λx：α.λy：β.x）

我们通过忽略所有的和他们的应用程序（和eliding typeannotations²），我们得到

  proj 1 = \p。 p（\xy  - > x）
  

或

  proj 1 p = p（\ x _  - > x）
  

我们的系统F版本有类型

proj 1：∀α.∀β。 α×β→α b
$ b

或者扩大

proj 1：∀α.∀β。 （∀γ.α→β→γ）→α

实际上，我们的Haskell版本的类型为

  proj 1 ::α**β - > α
  

再次展开为

  proj 1 ::（全部γ.α→β→γ）→> α
  

或者，使α和β显式，

  proj 1 :: forallαβ。 （全部γ.α→β→γ）→> α
  

为了完整性，我们也有

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

proj 2 =Λα.Λβ.λp：α×β.pβ（λx：α.λy：β.y）

<它变成了

  proj 2 ::α**β - >> β
proj₂p = p（\_y  - > y）
  

即在这一点上可能并不奇怪： - ）

---

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

²我们忽略Λ表示类型变量未被绑定在条款。以下是一个错误：

  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 
  

正常工作。

I want to implement the Church encoding of the pair in polymorphic lambda calculus in Haskell.

On page 77, section 8.3.3 of Peter Selinger's notes on lambda calculus, he gives a construction of the cartesian product of two types as

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

For another source, on page 54, section 4.2.3 of Dider Rémy's notes on lambda calculus, he defines the Church encoding of the pair in polymorphic λ-calculus/System F as

Λα₁.Λα₂.λx₁∶α₁.λx₂∶α₂.Λβ.λy∶α₁→α₂→β. y x₁ x₂

I think Rémy is saying the same thing, just more verbosely, as Selinger.

Anyway, according to Wikipedia, the type system for Haskell is based on System F, so I am hoping it is possible to implement this Church encoding directly in Haskell. I've got:

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

but I wasn't sure how to do the projections.

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

Do I use the Haskell forall for the capital lambda type quantifier?

This is basically the same as my previous question, but in Haskell instead of Swift. I thought the additional context and the change of venue might make it more sensible.

解决方案

First of all, you're indeed correct that Selinger and Rémy are saying the same thing; the difference is that Rémy is defining the pair constructor function ⟨–,–⟩, which takes as arguments M and N (his x₁ and x₂) along with their types (α₁ and α₂); the remainder of his definition is just the definition of ⟨M,N⟩ with β and y where Selinger has α and f.

Alright, with that taken care of, let's start moving towrads projections. The first thing to note is the relation between ∀, Λ, →, and λ, and their equivalents in Haskell. Recall that ∀ and its inhabitants Λ operate on types, where → and its inhabitants λ operate on values. Over in Haskell-land, most of these correspondences are easy, and we get the following 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

The term-level entries are easy: → becomes -> and λ becomes \. But what about ∀ and Λ?

By default, in Haskell, all the ∀s are implicit. Every time we refer to a type variable (a lower-case identifier in a type), it's implicitly universally quantified. So a type signature like

id :: a -> a

corresponds to

id : ∀α.α→α

in System F. We can turn on the language extension ExplicitForAll and gain the ability to write those explicitly:

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

By default, however, Haskell only lets us put those quantifiers at the start of our definitions; we want the System F-style ability to put foralls anywhere in our types. For this, we turn on RankNTypes. In fact, all Haskell code from now on will use

{-# LANGUAGE RankNTypes, TypeOperators #-}

(The other extension allows type names to be operators.)

Now that we know all that, we can try to write down the definition of ×. I'll call its Haskell version ** to keep things distinct (although we could use × if we wanted). Selinger's definition is

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

so the Haskell is

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

And as you said, the creation function is

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

But what happened to our Λs? They're there in the System F definition of ⟨M,N⟩, but pair doesn't have any!

So this is the last cell in our table: in Haskell, all Λs are implicit, and there's not even an extension to make them explicit.¹ Anywhere they would show up, we just ignore them, and type inference fills them in automatically. So, to answer one of your explicit questions directly, you use the Haskell forall to represent the System F ∀, and nothing to represent the System F type lambda Λ.

So you give the definition of the first projection as (reformatted)

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

We translate this to Haskell by ignoring all Λs and their applications (and eliding type annotations²), and we get

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

or

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

Our System F version has the type

proj₁ : ∀α.∀β. α×β → α

or, expanded

proj₁ : ∀α.∀β. (∀γ. α → β → γ) → α

and indeed, our Haskell version has the type

proj₁ :: α ** β -> α

which again expands to

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

or, to make the binding of α and β explicit,

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

And for completeness, we also have

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

which becomes

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

which is probably unsurprising at this point :-)

---

¹ Relatedly, all Λs can be erased at compile time – type information is not present in compiled Haskell code!

² The fact that we elide Λs means that type variables aren't bound in the terms. The following is an error:

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

because it's treated as though we'd written

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

which of course doesn't work. To get around this, we can turn on the language extension ScopedTypeVariables; then, any type variables bound in an explicit forall are in scope in the term. So the first example still breaks, but

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

works fine.

这篇关于在Haskell中实现多态λ演算/系统F对的教会编码的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！