HIMA' #5: 型推論 - PARTAKE Haskellが全然読めなくてちょっと面白かったです。 いくつか説明が抜けてたような気がしたので、勝手に補足。 多相型の定義 普通、MLとかHaskellとかでは、ネストした多相型は推論されません*1。 ∀α . α → αはOKですが、 ∀α. (∀β. β → β) → αはダメです。 この制限をうまいこと表現するために、「型(Type)」と「型スキーム(Type scheme)」という二つの概念を使って、「型」を表現することが広く行われています。 τ ::= Int | String | α | τ → τ | ... σ ::= τ | ∀α... . τここでτが型で、σが型スキームです。これを見ると、σはτそのものかτに束縛変数と総称量化子を付けたもののどちらかしか許されないことがわかります。つまり、∀をネストすることはできません