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

Question

我想在Haskell中的多态lambda演算中实现该对的Church编码.

在Peter Selinger关于lambda演算的注释的第77页第8.3.3节中,他给出了两种类型的笛卡尔积的构造.

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

对于另一个来源,在第54页,DiderRémy关于lambda演算的注释的第4.2.3节,他将多态λ演算/系统F中的对的教会编码定义为

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

我认为雷米和塞林格一样,更加啰嗦.

无论如何,根据维基百科,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类型量词？

这与我之前的问题基本相同,但在Haskell而不是Swift中.我认为额外的环境和场地的变化可能会让它变得更加明智.

Answer 1

首先,你确实是正确的,Selinger和Rémy说同样的话; 区别在于Rémy定义了对构造函数 ⟨ - , - ⟩,它将M和N(他的x 1和x 2)与它们的类型(α1和α2)作为参数; 他定义的其余部分只是⟨M,N⟩与β和y的定义,其中Selinger有α和f.

好吧,有了这个照顾,让我们开始移动towrads投影.首先要注意的是∀,Λ,→和λ之间的关系,以及它们在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中,所有的are都是隐式的.每当我们引用一个类型变量(一个类型中的小写标识符)时,它就会被隐含地普遍量化.所以类型签名就像

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

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

所以这是我们表格中的最后一个单元格:在Haskell中,所有的Λ都是隐含的,甚至没有一个扩展来使它们显式化.¹它们出现的任何地方,我们只是忽略它们,类型推断自动填充它们.因此,要直接回答您的一个显式问题,您可以使用Haskell forall来表示系统F∀,而无需表示系统F类型lambdaΛ.

所以你给第一个投影的定义为(重新格式化)

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

我们通过忽略所有Λs 及其应用(以及eliding typeannotations²)将其转换为Haskell ,我们得到

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

要么

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

我们的System F版本有类型

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

或者,扩大

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

事实上,我们的Haskell版本具有类型

proj? :: ? ** ? -> ?

再次扩展到

proj? :: (forall ?. ? -> ? -> ?) -> ?

或者,为了使绑定?和?显式,

proj? :: forall ? ?. (forall ?. ? -> ? -> ?) -> ?

为了完整起见,我们也有

proj 2:∀α.∀β.α×β→
βproj2 =Λα.Λβ.λ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

工作良好.