Implement in Haskell the Church encoding of the pa

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.

回答1:

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)

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.

回答2:

You wrote

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

Just remove all the type arguments, both in application and abstraction:

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

In Haskell, without type annotations:

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