System F
1972年
定義
bnf項t = x
| λx:A.t
| Λα.t // genricな型
| t t // 関数適用
| t[A] // 型適用. `[]`をつけずにtAと書くこともある
型A = α
| A1 -> A2
| ∀α.A
文脈Γ = <>
| <Γ,x:A>
補足
α は型変数
x は変数
Λ は型レベルのラムダ抽象
つまりGenricな型のこと
型を引数に取り、型を返す
Λt.t というラムダ抽象を型 t1 に適用して、 t1 になる感じ
λ は値レベルのラムダ抽象
λx:A.t は、括弧を付けるなら λ(x:A).t
引数 x が A で型付けされることで定義域が明示されている
「項t」は、「値レベルのラムダ抽象」と、「型レベルのラムダ抽象」の両方を表す
変数には値のみが代入でき、型変数には型のみが代入できる、という前提がある
t[A] は型 A を関数 t に代入しているが、これは暗黙的に t は Λ で表現される方のラムダ抽象である
この表記はTaPLに倣っている
一般的には角括弧は書かずに tA と書く
つまり小文字か大文字かで、関数適用か型適用かを判断する
例
恒等関数idをSystem Fで書く
id = Λa.λ(x:a).x
このとき id: ∀α.α->α
まずなんらかの型を適用することで、その型に対する恒等関数にする
idBool = id Bool = λx:Bool.x
Bool型を適用することで、Bool型用のidにした
関連
参考
一番わかり易い