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.
