首先，Selinger 和 Rémy 说的是同一件事，这确实是正确的；不同之处在于，Rémy 定义了对构造函数⟨–,–⟩，它将 M 和 N（他的 x₁ 和 x₂）及其类型（α₁ 和 α₂）作为参数；他定义的其余部分只是 ⟨M,N⟩ 的定义，其中有 β 和 y，其中 Selinger 有 α 和 f。
好吧，处理完这些，让我们开始向预测移动。首先要注意的是∀、Λ、→和λ之间的关系，以及它们在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 中，所有的 ∀ 都是隐式的。每次我们引用类型变量（类型中的小写标识符）时，它都会被隐式地普遍量化。所以类型签名像
id :: a -> a
对应于
id : ∀α.α→α</p>
在 System F 中。我们可以打开语言扩展ExplicitForAll并获得明确编写这些的能力：
{-# LANGUAGE ExplicitForAll #-}
id :: forall a. a -> a
然而，默认情况下，Haskell 只允许我们将这些量词放在定义的开头；我们希望 System F 风格的能力可以将foralls 放在我们的类型中的任何位置。为此，我们打开RankNTypes. 事实上，从现在开始，所有 Haskell 代码都将使用
{-# LANGUAGE RankNTypes, TypeOperators #-}
（另一个扩展允许类型名称是运算符。）
既然我们都知道了，我们可以试着写下×的定义。我将其称为 Haskell 版本**以保持不同（尽管我们可以×根据需要使用）。塞林格的定义是
A×B = ∀α.(A→B→α)→α</p>
所以 Haskell 是
type a ** b = forall α. (a -> b -> α) -> α
正如你所说，创造功能是
pair :: a -> b -> a ** b
pair x y f = f x y
但是我们的 Λ 怎么了？它们存在于 ⟨M,N⟩ 的 System F 定义中，但pair没有！
所以这是我们表中的最后一个单元格：在 Haskell 中，所有 Λ 都是隐式的，甚至没有扩展来使它们显式。¹任何它们会出现的地方，我们只是忽略它们，类型推断会自动填充它们。因此，要直接回答您的明确问题之一，您使用 Haskellforall来表示 System F ∀，而没有任何内容来表示 System F 类型 lambda Λ。
因此，您将第一个投影的定义定义为（重新格式化）
proj₁ = Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
我们通过忽略所有 Λ及其应用程序（以及省略类型注释²）将其转换为 Haskell，我们得到
proj₁ = \p. p (\x y -> x)
或者
proj₁ p = p (\x _ -> x)
我们的 System F 版本具有类型
proj₁：∀α.∀β。α×β → α
或者，展开
proj₁：∀α.∀β。(∀γ. α → β → γ) → α
确实，我们的 Haskell 版本有这样的类型
proj₁ :: α ** β -> α
再次扩展到
proj₁ :: (forall γ. α -> β -> γ) -> α
或者，使绑定α和β明确，
proj₁ :: forall α β. (forall γ. α -> β -> γ) -> α
为了完整起见，我们还有
proj₂：∀α.∀β。α×β → β
proj₂ = Λα.Λβ.λ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
工作正常。