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

はじめに

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

• Mark P Jones: Typing Haskell in Haskell
• MokkosuでHaskellの型システムを作る (その1)
• MokkosuでHaskellの型システムを作る (その2)
• MokkosuでHaskellの型システムを作る (その3)
• MokkosuでHaskellの型システムを作る (その4)

前回までは論文に載っている Haskell のコードを Mokkosu に移植する作業を行ってきました。今回からは、移植した Mokkosu のコードを論文を読みながら解読していきます。

1. Introduction

• この記事ではMokkosuを仕様記述言語としてHaskellの型システムの説明を試みる。
• 最低限MokkosuとHaskellのプログラムが読めることを前提条件とする。
• ここで得られた知識を基に、Mokkosuに型クラスを導入したい。

2. Preliminaries

include "List.mok";

• ここでは標準ライブラリの関数に加え、リストライブラリの関数を使う。
• 変数名や型変数名などの識別子には文字列(String)を用いる。

let new_id =
  let cnt = ref 0 in
  \() ->
    do incr cnt in
    "$" ^ to_string !cnt;

new_id : () -> String

• new_id関数は新しい識別子の名前を作る関数。
• ソースファイルの変数名は$から始まらないこととする。

3. Kinds

• カインドとは型をその種類に応じて分類したもの。
• IntやChar -> Boolなどのシンプルな型式はカインド*で表す。
• k1、k2をカインドとしたときk1 -> k2の形式のカインドは型コンストラクタを表す。
• 例えば、MaybeやIOはカインド* -> *で表す。

type Kind = Star
          | Kfun (Kind, Kind);

• カインド*はStarで、k1 -> k2はKfun(k1, k2)と表すこととする。

fun kind_equal k1 k2 =
  match (k1, k2) {
    (~Star, ~Star) -> true;
    (~Kfun(k11,k12), ~Kfun(k21,k22)) ->
      kind_equal k11 k21 && kind_equal k12 k22;
    _ -> false
  };

kind_equal : Kind -> Kind -> Bool

• kind_equal関数は与えられた2つのカインドが等しいかどうかを判定する関数。

4. Types

type Tyvar = Tyvar (String, Kind);

• Tyvarは型変数(型に関する変数)を表す。
• 型変数は文字列で区別しカインドをもつ。

fun tyvar_equal ~Tyvar(id1,k1) ~Tyvar(id2,k2) =
  id1 == id2 && kind_equal k1 k2;

tyvar_equal : Tyvar -> Tyvar -> Bool

• tyvar_equalは与えられた2つの型変数が等しいかどうかを判定する関数。
• 名前とカインドが等しければ与えられた2つの型変数は等しい。
• 実際には名前が同じでカインドが異なる型変数は存在しない。

type Tycon = Tycon (String, Kind);

• Tyconは型コンストラクタを表す。
• 型コンストラは文字列で区別しカインドをもつ。

fun tycon_equal ~Tycon(id1,k1) ~Tycon(id2,k2) =
  id1 == id2 && kind_equal k1 k2;

tycon_equal : Tycon -> Tycon -> Bool

• tycon_equalは与えられた2つの型コンストラクタが等しいかどうかを判定する関数。
• 名前とカインドが等しければ与えられた2つの型コンストラクタは等しい。
• 実際には名前が同じでカインドが異なる型コンストラクタは存在すべきではない。
  • 今回の実装では名前が同じでカインドが異なる型コンストラクタは許しているようである。(要確認)
  • 少なくともGHCでは名前が同じでカインドが異なる型コンストラクタはエラーとなった。

type Type = TVar (Tyvar)
          | TCon (Tycon)
          | TAp (Type, Type)
          | TGen (Int);

• TVarは型変数。
• TConは型コンストラクタ。
• TApは型への型コンストラクタの適用。
• TGenはのちに出てくる型スキーム内で多相になった型変数を示すのに使うのでしばらくは忘れてよい。

fun type_equal t1 t2 =
  match (t1, t2) {
    (~TVar(tv1), ~TVar(tv2)) ->
      tyvar_equal tv1 tv2;
    (~TCon(tc1), ~TCon(tc2)) ->
      tycon_equal tc1 tc2;
    (~TAp(t11, t12), ~TAp(t21, t22)) ->
      type_equal t11 t21 && type_equal t12 t22;
    (~TGen(i1), ~TGen(i2)) ->
      i1 == i2;
    _ ->
      false
  };

type_equal : Type -> Type -> Bool

• type_equalは与えられた2つの型が等しいかどうかを判定する関数。

let t_unit = TCon (Tycon ("()", Star));

t_unit : Type

• 上で定義したデータ型を用いてHaskellの()型を表した例。

let t_char = TCon (Tycon ("Char", Star));
let t_int = TCon (Tycon ("Int", Star));
let t_integer = TCon (Tycon ("Integer", Star));
let t_float = TCon (Tycon ("Float", Star));
let t_double = TCon (Tycon ("Double", Star));

t_char : Type
t_int : Type
t_integer : Type
t_float : Type
t_double : Type

• 同様に、Char、Int、Integer、Float、Double型を表した例。

let t_list = TCon (Tycon ("[]", Kfun (Star, Star)));
let t_arrow = TCon (Tycon ("(->)", Kfun (Star, Kfun (Star, Star))));
let t_tuple2 = TCon (Tycon ("(,)", Kfun (Star, Kfun (Star, Star))));

t_list : Type
t_arrow : Type
t_tuple2 : Type

• リストのコンストラクタ[]、関数の型コンストラクタ(->)、2要素タプルの型コンストラクタ(,)を表した例。

let fn a b = TAp (TAp (t_arrow, a), b);
let list t = TAp (t_list, t);
let pair a b = TAp (TAp (t_tuple2, a), b);

fn : Type -> Type -> Type
list : Type -> Type
pair : Type -> Type -> Type

• 関数型、リスト型、2要素タプル型を作る補助関数。

let t_string = list t_char;

t_string : Type

• 文字列型の例。文字列は文字のリストで表す。

let tyvar_kind ~Tyvar(_, k) = k;

tyvar_kind : Tyvar -> Kind

• tyvar_kindは型変数のカインドを返す関数。

let tycon_kind ~Tycon(_, k) = k;

tycon_kind : Tycon -> Kind

• tycon_kindは型コンストラクタのカインドを返す関数。

fun type_kind = {
  ~TCon(tc) -> tycon_kind tc;
  ~TVar(tv) -> tyvar_kind tv;
  ~TAp(t,_) ->
    match (type_kind t) {
      ~Kfun(_, k) -> k
    }
};

type_kind : Type -> Kind

• type_kindは型のカインドを返す関数。
• TAp(t1,t2)の時はカインドの整合が取れているという前提のもと、t1のカインドk1 -> k2のk2部分を返す。

5. Substitution

type Subst = Subst ([(Tyvar, Type)]);

• 代入は型変数から型への写像。
• ここでは型変数と型のタプルのリストで表す。

let subst_null = Subst ([]);

subst_null : Subst

• subst_nullはからの代入を表す定数。
• 空の代入は空リストを使って表す。

let subst_single tv t = Subst ([(tv, t)]);

subst_single : Tyvar -> Type -> Subst

• subst_singleは型変数tvを型tに対応付けるだけの代入を作る関数。

let subst_lookup tv s =
  fun loop = {
    [] -> Nothing;
    (tv1,t) :: _ ? tyvar_equal tv tv1 -> Just (t);
    _ :: rest -> loop rest
  } in
  let ~Subst(list) = s in
  loop list;

subst_lookup : Tyvar -> Subst -> Maybe<Type>

• subst_lookupは代入から型変数に対応する型を探索する。

fun tyvar_list_elem tv = {
  [] -> false;
  tv1 :: rest -> tyvar_equal tv tv1 && tyvar_list_elem tv rest
};

tyvar_list_elem : Tyvar -> [Tyvar] -> Bool

• tyvar_list_elem関数は型変数が型変数のリストに含まれるかどうかを判定する関数。

fun tyvar_list_union l1 l2 =
  match l1 {
    [] -> l2;
    tv :: rest ->
      if tyvar_list_elem tv l2 ->
        tyvar_list_union rest l2
      else
        tv :: tyvar_list_union rest l2
  };

tyvar_list_union : [Tyvar] -> [Tyvar] -> [Tyvar]

• 型変数のリストを型変数の集合にみたてて、2つの集合の和を求める。

fun tyvar_list_intersect l1 l2 =
  match l1 {
    [] -> [];
    tv :: rest ->
      if tyvar_list_elem tv l2 ->
        tv :: tyvar_list_union rest l2
      else
        tyvar_list_union rest l2
  };

tyvar_list_intersect : [Tyvar] -> [Tyvar] -> [Tyvar]

• 型変数のリストを型変数の集合にみたてて、2つの集合の共通部分を求める。

let tyvar_list_nub list =
  fun loop list = {
    [] -> list;
    tv :: rest ->
      if tyvar_list_elem tv list ->
        loop list rest
      else
        loop (tv :: list) rest
  } in
  loop [] list;

tyvar_list_nub : [Tyvar] -> [Tyvar]

• 型変数のリストの重複を取り除く。

fun type_apply s = {
  ~TVar(tv) ->
    match (subst_lookup tv s) {
      ~Just(t) -> t;
      ~Nothing -> TVar(tv)
    };
  ~TAp(f,a) ->
    TAp (type_apply s f, type_apply s a);
  t -> t
};

type_apply : Subst -> Type -> Type

• 代入を型に適用する。

let type_list_apply s = map (type_apply s);

type_list_apply : Subst -> [Type] -> [Type]

• 代入を型のリストに適用する。

fun type_tv = {
  ~TVar(tv) -> [tv];
  ~TAp(f,a) -> type_tv f `tyvar_list_union` type_tv a;
  t -> []
};

type_tv : Type -> [Tyvar]

• 型に含まれる型変数をリスト(集合)にして返す。

let type_list_tv = tyvar_list_nub << concat << map type_tv;

type_list_tv : [Type] -> [Tyvar]

• 型のリストに含まれる型変数をリスト(集合)にして返す。

let subst_append (~Subst(l1) as s1) (~Subst(l2) as s2) =
  Subst <| (for (tv, t) <- l2 in (tv, type_apply s1 t)) ++ l1;

subst_append : Subst -> Subst -> Subst

• 与えられた2つの代入を連結する。
• apply (subst_append s1 s2) == apply s1 << apply s2 を満たすように連結する。
• つまり、s2を適用してs1を適用するような代入を返す。

let subst_merge (~Subst(l1) as s1) (~Subst(l2) as s2) =
  let agree =
    all (\v -> type_apply s1 (TVar v) `type_equal` type_apply s2 (TVar v))
        (map fst l1 `tyvar_list_intersect` map fst l2)
  in
  if agree -> Subst (l1 ++ l2) else error "merge fails";

subst_merge : Subst -> Subst -> Subst

• 与えられた2つの代入をマージする。
• +++を代入のリストを単純に連結する関数としたとき、apply (s1 +++ s2) == apply (s2 +++ s1)を満たす場合のみマージする。

6. Unification and Matching

• 単一化(unification)とは2つの型を等しくする代入を見つけること。
• 単に等しくする代入を見つけるだけでなく、可能な限り小さな代入を見つける。
• 可能な限り小さな代入はもっとも一般的な型を導く。
• もしtype_apply s t1 == type_apply s t2となるときsは単一化子(unifier)とよぶ。
• 最も一般的な単一化子(mgu, most general unifier)とは、どんな単一化子sに対しても、subst_append s1 uとなる代入s1が存在するような単一化子uのことをいう。
• Haskellの構文は2つの型が単一化子を持つ場合は、最も一般的な単一化子が存在するよう設計されている。
• Haskellは型の別名を定義するときに部分適用を認めていないが、これを認めると最も一般的な単一化子が求まらなくなる。

let var_bind tv t = 
  match t {
    ~TVar(tv2) ? tyvar_equal tv tv2 ->
      subst_null;
    _ ? tyvar_list_elem tv (type_tv t) ->
      error "occurs check fail";
    _ ? not (kind_equal (tyvar_kind tv) (type_kind t)) ->
      error "kinds do not match";
    _ ->
      subst_single tv t
};

var_bind : Tyvar -> Type -> Subst

• var_bind関数はsubst_single関数同様、型変数tvを型tに対応付けるだけの代入を作る関数であるが、いくつか追加の検査を行う。
• もし同じ型変数の場合は空の代入を返す。
• 型自身に型変数が含まれている場合(出現違反)エラーにする。
• 型変数と型のカインドが異なる場合エラーにする。

fun mgu t1 t2 =
  match (t1, t2) {
    (~TAp(f1,a1), ~TAp(f2,a2)) ->
      let s1 = mgu f1 f2 in
      let s2 = mgu (type_apply s1 a1) (type_apply s1 a2) in
      subst_append s1 s2;
    (~TVar(tv), t) ->
      var_bind tv t;
    (t, ~TVar(tv)) ->
      var_bind tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 ->
      subst_null;
    _ ->
      error "types do not unify"
  };

mgu : Type -> Type -> Subst

• mgu関数は与えられた2つの型のもっとも一般的な単一化子を返す。
• 両辺が型コンストラクタの適用の場合、コンストラクタ部と引数部をそれぞれ単一化してそれらを結合する。
• コンストラクタ部単一化によって得られた代入を、引数の型に適用しておく必要がある点に注意。
• 片方が型変数の場合、型変数から型への対応だけからなる代入を作る。
• 両辺が同じ型コンストラクタ(型)の場合は空の代入を返す。
• それ以外は単一化エラー。

fun type_match t1 t2 =
  match (t1, t2) {
    (~TAp(f1,a1), ~TAp(f2,a2)) ->
      let s1 = type_match f1 f2 in
      let s2 = type_match a1 a2 in
      subst_merge s1 s2;
    (~TVar(tv), t) ? kind_equal (tyvar_kind tv) (type_kind t) ->
      subst_single tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 ->
      subst_null;
    _ ->
      error "type do not match"
  };

type_match : Type -> Type -> Subst

• マッチングとはtype_apply s t1 == t2となるような代入sを見つける操作。
• type_matchは第1引数の型に適用すると第二引数の型になるような代入を見つける関数。
• 型コンストラクタの時はそれぞれのマッチングを求めて代入をマージする。
• 型変数の時はカインドが等しいことをチェックして単一の代入を返す。
• 同じ型の時は空の代入を返す。
• それ以外の場合はマッチングエラーにする。

つづく。