MokkosuでHaskellの型システムを作る (その8)

# はじめに

Simon Peyton Jones の論文 Typing Haskell in Haskell を参考に Haskell の型システムの実装に挑戦しています。実装には関数型言語の [Mokkosu](http://lambdataro.sakura.ne.jp/mokkosu/) を使っています。

* [Mark P Jones: Typing Haskell in Haskell](http://web.cecs.pdx.edu/~mpj/thih/)
* [MokkosuでHaskellの型システムを作る (その1)](http://qiita.com/lambdataro/items/1e4d795d3dd97a94c8f3)
* [MokkosuでHaskellの型システムを作る (その2)](http://qiita.com/lambdataro/items/c19e0d6d637e0dbb52ca)
* [MokkosuでHaskellの型システムを作る (その3)](http://qiita.com/lambdataro/items/681cabee9c307b0d5e3e)
* [MokkosuでHaskellの型システムを作る (その4)](http://qiita.com/lambdataro/items/ffe1544b13b5b5458b4c)
* [MokkosuでHaskellの型システムを作る (その5)](http://qiita.com/lambdataro/items/2018737b9d578600c222)
* [MokkosuでHaskellの型システムを作る (その6)](http://qiita.com/lambdataro/items/e1ba95453ac10c6c308e)
* [MokkosuでHaskellの型システムを作る (その7)](http://qiita.com/lambdataro/items/d56b776d9640789c0480)

前回に引き続き、Haskellから移植したMokkosuコードを解読していきます。

# 8. Type Schemes
```
type Scheme = Forall ([Kind], Qual<Type>);
```
* 型スキームです。
* forallが付く型は、`TGen`コンストラクタを用いて表します。
* `TGen`コンストラクタはカインドのリストのn番目を指します。

```
let kind_list_equal ks1 ks2 =
  length ks1 == length ks2 &&
  all (uncurry kind_equal) (zip ks1 ks2);
```
```
kind_list_equal : [Kind] -> [Kind] -> Bool
```
* 与えられた2つのカインドのリストが等しいかどうかを判定します。

```
let scheme_equal ~Forall(ks1,q1) ~Forall(ks2,q2) =
  kind_list_equal ks2 ks2 && qual_type_equal q1 q2;
```
```
scheme_equal : Scheme -> Scheme -> Bool
```
* 与えられた2つの型スキームが等しいかどうかを判定します。

```
let scheme_apply s ~Forall(ks,qt) =
  Forall (ks, qual_type_apply s qt);
```
```
scheme_apply : Subst -> Scheme -> Scheme
```
* 型スキームに代入を適用します。

```
let scheme_tv ~Forall(ks,qt) =
  qual_type_tv qt;
```
```
scheme_tv : Scheme -> [Tyvar]
```
* 型スキーム中の型変数の集合を返します。

```
let quantify vs qt =
  let vs2 = for v <- qual_type_tv qt;
                if tyvar_list_elem v vs in v
  in
  let ks = map tyvar_kind vs2 in
  let s = Subst (zip vs2 (map TGen (0 .. length vs2))) in
  Forall (ks, qual_type_apply s qt);
```
```
quantify : [Tyvar] -> Qual<Type> -> Scheme
```
* `quantify`関数は型クラスで修飾された型にforallを付けます。
* forallを付ける型は、型変数のうち関数の第一引数のリストに含まれるものに限ります。
* カインドのリストの順番は引数の型クラスで修飾された型の構造に依存します。

```
let to_scheme t =
  Forall ([], Qual ([], t));
```
```
to_scheme : Type -> Scheme
```
* 型をforallをつけずに型スキームにします。

# 9. Assumptions
```
type Assump = Assump (String, Scheme);
```
* 変数に対してどのような型が割り当てらているのかを表すデータ構造です。

```
let assump_apply s ~Assump(i,sc) = 
  Assump (i, scheme_apply s sc);
```
```
assump_apply : Subst -> Assump -> Assump
```
* `Assump`型の値に対して代入を適用します。

```
let assump_tv ~Assump(i,sc) =
  scheme_tv sc;
```
```
assump_tv : Assump -> [Tyvar]
```
* `Assump`型の値に含まれる自由変数の集合を返します。

# 10. A Type Inference Monad

```
let subst = ref subst_null;
```
```
subst : Ref<Subst>
```
* 現在の代入を格納するグローバル変数です。

```
let get_subst () = !subst;
```
```
get_subst : () -> Subst
```
現在の代入を取得します。

```
let ext_subst s2 =
  subst := s2 `subst_append` !subst;
```
```
ext_subst : Subst -> ()
```
* 指定した代入で現在の代入を拡張します。

```
let unify t1 t2 =
  let s = get_subst () in
  let u = mgu (type_apply s t1) (type_apply s t2) in
  ext_subst u;
```
* 与えられた2つの型を単一化します。

```
let new_tvar k =
  TVar (Tyvar (new_id (), k));
```
```
new_tvar : Kind -> Type
```
* 新しい型変数を作ります。

```
fun inst_type ts = {
  ~TAp(l,r) -> TAp(inst_type ts l, inst_type ts r);
  ~TGen(n) -> nth ts n;
  t -> t
};
```
```
inst_type : [Type] -> Type -> Type
```
* 型を与えられた具体的な型でインスタンシエートします。
* 具体的には型に含まれる`TGen`の置き換えを行います。

```
let inst_pred ts ~IsIn(c,t) =
  IsIn(c, inst_type ts t);
```
```
inst_pred : [Type] -> Pred -> Pred
```
* 述語をインスタンシエートします。

```
let inst_pred_list ts ps =
  map (inst_pred ts) ps;
```
```
inst_pred_list : [Type] -> [Pred] -> [Pred]
```
* 述語のリストをインスタンシエートします。

```
let inst_qual ts ~Qual(ps,t) =
  Qual(inst_pred_list ts ps, inst_type ts t);
```
```
inst_qual : [Type] -> Qual<Type> -> Qual<Type>
```
* 型クラスで修飾された型をインスタンシエートします。

```
let fresh_inst ~Forall(ks,qt) =
  let ts = map new_tvar ks in
  inst_qual ts qt;
```
```
fresh_inst : Scheme -> Qual<Type>
```
* 型スキームからインスタンシエートした型クラスで修飾された型を作ります。

つづく