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⟩ = Λα.λfA→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
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
corresponds to
id : ∀α.α→α
in System F. We can turn on the language extension
ExplicitForAll
and gain the ability to write those explicitly: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
forall
s anywhere in our types. For this, we turn onRankNTypes
. In fact, all Haskell code from now on will use(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 isA×B = ∀α.(A→B→α)→α
so the Haskell is
And as you said, the creation function is
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
or
Our System F version has the type
proj₁ : ∀α.∀β. α×β → α
or, expanded
proj₁ : ∀α.∀β. (∀γ. α → β → γ) → α
and indeed, our Haskell version has the type
which again expands to
or, to make the binding of
α
andβ
explicit,And for completeness, we also have
proj₂ : ∀α.∀β. α×β → β
proj₂ = Λα.Λβ.λp:α×β.p β (λx:α.λy:β.y)
which becomes
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:
because it's treated as though we'd written
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 explicitforall
are in scope in the term. So the first example still breaks, butworks fine.
You wrote
Just remove all the type arguments, both in application and abstraction:
In Haskell, without type annotations: