はじめに

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

Mark P Jones: Typing Haskell in Haskell

論文にあるコードをそのままMokkosuに移植しただけです。

識別子

type Id = Id (String);

fun id_equal id1 id2 =
  match (id1, id2) {
    (~Id(s1), ~Id(s2)) -> s1 == s2
  };

let enum_id (n : Int) = Id ("v" ^ to_string n);

カインド

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

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;
  };

型

type Tyvar = Tyvar (Id, Kind);

fun tyvar_equal tv1 tv2 =
  match (tv1, tv2) {
    (~Tyvar(id1,k1), ~Tyvar(id2,k2)) ->
      id_equal id1 id2 && kind_equal k1 k2
  };

type Tycon = Tycon (Id, Kind);

fun tycon_equal tc1 tc2 =
  match (tc1, tc2) {
    (~Tycon (id1,k1), ~Tycon(id2,k2)) ->
      id_equal id1 id2 && kind_equal k1 k2    
  };

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

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    
  };

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

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

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);

let t_string = list t_char;

let kind_tyvar = {
  ~Tyvar (_, k) -> k
};

let kind_tycon = {
  ~Tycon (_, k) -> k
};

fun kind_type = {
  ~TCon(tc) -> kind_tycon tc;
  ~TVar(tv) -> kind_tyvar tv;
  ~TAp(t,_) ->
    match (kind_type t) {
      ~Kfun(_, k) -> k
    }
};

代入

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

let null_subst = Subst([]);

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

let lookup_subst tv s =
  fun loop = {
    [] -> Nothing;
    (tv1,typ) :: _ ? tyvar_equal tv tv1 -> Just (typ);
    _ :: rest -> loop rest
  }
  in
  let ~Subst(list) = s in
  loop list;
  
fun apply_type s t =
  match t {
    ~TVar(tv) ->
      match (lookup_subst tv s) {
        ~Just(t) -> t;
        ~Nothing -> TVar(tv)
      };
    ~TAp(l,r) -> TAp (apply_type s l, apply_type s r);
    _ -> t
  };

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

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

fun tv_type = {
  ~TVar(tv) -> [tv];
  ~TAp(l,r) -> tv_type l `union_tyvar_list` tv_type r;
  t -> []
};

let apply_type_list s = map (apply_type s);

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

let tv_type_list = nub_tyvar_list << concat << map tv_type;

let append_subst s1 s2 =
  let ~Subst(l1) = s1 in
  let ~Subst(l2) = s2 in
  let l3 = (for (tv, t) <- l2 in (tv, apply_type s1 t)) ++ l1 in
  Subst (l3);

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

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

ここまでの感想

Mokkosuにはderiving Eq相当のものが存在しないため、データコンストラクタを作るたびに**_equal関数を作る必要があった。
Mokkosuには型クラスがないため、代入の関数などは実装ごとに別の名前を付ける必要があった。個人的には型ごとに別の名前が付いていた方が分かりやすいように思う。
データコンストラクタの等価性を専用の関数を使って判定する必要があるため、いくつかのリスト操作関数は型に特化したものを実装しなおす必要があった。

つづく。