HIMA' #5に行ってきたよ
Haskellが全然読めなくてちょっと面白かったです。
いくつか説明が抜けてたような気がしたので、勝手に補足。
多相型の定義
普通、MLとかHaskellとかでは、ネストした多相型は推論されません*1。
∀α . α → α
はOKですが、
∀α. (∀β. β → β) → α
はダメです。
この制限をうまいこと表現するために、「型(Type)」と「型スキーム(Type scheme)」という二つの概念を使って、「型」を表現することが広く行われています。
τ ::= Int | String | α | τ → τ | ... σ ::= τ | ∀α... . τ
ここでτが型で、σが型スキームです。これを見ると、σはτそのものかτに束縛変数と総称量化子を付けたもののどちらかしか許されないことがわかります。つまり、∀をネストすることはできません。
型環境
そもそも型推論というのはいったいなんなのか、というと、
型環境Γ、式eが与えられたときに、式eの型τを求める手続き
のことです。他にもいくつか表現がありますが、だいたいこんな感じです。
これに関連して、「型判定(typing judgement)」という概念もあります。
型環境Γ、式e、型τが与えられたときに、式eの型は本当にτで良かったよ!
というものです。
Γ |- e : τ
という形で書くことが多いです。
この型判定を導出するための規則を、「型付け規則」とか呼んだりします。
型環境というのは、変数の型を保存しておくやつで、変数名と型スキームの組の集合です。
let多相
Haskellのwhereとかはlet (rec)で書けるよねーという話は済んでいると仮定して。
ML/Haskellの型推論において多相型が出てくるのは、letで式が変数を束縛したときだけです。
式の型、は常に「型」です。つまり、単相です。それでは多相型はどこで出てくるのかというと、「変数そのものの型」として出てきます(型環境は変数名→型スキームの写像)。つまり、letで束縛された変数が多相型になる。「変数」というのは、実は式のこともあるので、「そのもの」と付けました。
Generalizationの仮定
Generalizationの手続きで、
α→β
を
∀αβ . α→β
にするときには、一つ仮定があります。
それは、αもβも型環境に自由な型変数として表れないことです。これは、関数の抽象のときにも同じですね。
まとめ
なんとなく説明が抜けてるかなーと思ったことをまとめました。最初から聞いてなかったので、最初の方に説明してたよ!とかいう場合はごめんなさい。あとラムダプラスも読んでないので、みんな読んでたから100も承知だったよ!というときもごめんなさい。後で読みます。
*1:実際には、いろいろと研究がされているので、うまいこと推論してくれる処理系があるかもしれませんが、原則としてはされません
