まず第一に、セリンジャーとレミーが同じことを言っているのは確かに正しいです。違いは、Rémy がペア コンストラクター関数⟨–,–⟩ を定義していることです。これは引数として M と N (彼の x₁ と x₂) とそれらの型 (α₁ と α₂) を受け取ります。彼の定義の残りの部分は、β と y を持つ⟨M,N⟩ の定義であり、セリンガーは α と f を持っています。
よし、それが終わったら、ラズプロジェクションに移りましょう。最初に注意すべきことは、∀、Λ、→、および λ と Haskell での同等の関係です。∀ とその住民 Λ は型を操作し、ここで → とその住民 λ は値を操作することを思い出してください。Haskell ランドでは、これらの対応のほとんどは簡単で、次の表が得られます。
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>
システム F で。言語拡張機能をオンにして、ExplicitForAllそれらを明示的に記述できるようにすることができます。
{-# LANGUAGE ExplicitForAll #-}
id :: forall a. a -> a
しかしデフォルトでは、Haskell はこれらの量指定子を定義の最初に置くことしかできません。forall型のどこにでも sを配置できる System F スタイルの機能が必要です。このために、 をオンにしRankNTypesます。実際、今後すべての Haskell コードは
{-# LANGUAGE RankNTypes, TypeOperators #-}
(他の拡張では、型名を演算子にすることができます。)
これですべてがわかったので、×の定義を書き留めてみることができます。Haskell バージョンと呼んで**区別しておきます (ただし、必要×に応じて使用することもできます)。セリンジャーの定義は、
A×B = ∀α.(A→B→α)→α</p>
だからハスケルは
type a ** b = forall α. (a -> b -> α) -> α
そして、あなたが言ったように、作成機能は
pair :: a -> b -> a ** b
pair x y f = f x y
しかし、私たちのΛはどうなりましたか？それらは ⟨M,N⟩ の System F 定義にありますが、pair何もありません!
したがって、これが表の最後のセルです。Haskell では、すべての Λ は暗黙的であり、明示的にするための拡張さえありません¹。それらが現れる場所はどこでも無視し、型推論によって自動的に埋められます。したがって、明示的な質問の 1 つに直接答えるには、Haskellforallを使用してシステム F ∀を表し、システム F タイプのラムダ Λ を表すものは何も使用しません。
したがって、最初の投影の定義を (再フォーマット) として指定します。
proj₁ = Λα.Λβ.λp:α×β.p α (λx:α.λy:β.x)
これをすべての Λとその適用を無視して(そして型注釈² を省略して) Haskell に変換すると、次のようになります。
proj₁ = \p. p (\x y -> x)
また
proj₁ p = p (\x _ -> x)
私たちのシステム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
正常に動作します。