はじめに

Simon Peyton Jones の論文 Typing Haskell in Haskell を参考に Haskell の型システムの実装に挑戦しています。実装には関数型言語の Mokkosu を使っています。

前回に引き続き、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>

型スキームからインスタンシエートした型クラスで修飾された型を作ります。

つづく

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

はじめに

8. Type Schemes

9. Assumptions

10. A Type Inference Monad