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

はじめに

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

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

単一化

let var_bind tv t =
  match t {
    ~TVar(tv2) ? tyvar_equal tv tv2 ->
      null_subst;
    _ ? mem_tyvar_list tv (tv_type t) ->
      error "occurs check fail";
    _ ? not (kind_equal (kind_tyvar tv) (kind_type t)) ->
      error "kinds do not match";
    _ ->
      single_subst tv t
  };

fun mgu t1 t2 =
  match (t1, t2) {
    (~TAp(l1,r1), ~TAp(l2,r2)) ->
      let s1 = mgu l1 l2 in
      let s2 = mgu (apply_type s1 r1) (apply_type s1 r2) in
      append_subst s1 s2;
    (~TVar(tv), t) -> var_bind tv t;
    (t, ~TVar(tv)) -> var_bind tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 -> null_subst;
    _ -> error "types do not unify"
  };

fun match_type t1 t2 =
  match (t1, t2) {
    (~TAp(l1,r1), ~TAp(l2,r2)) ->
      let sl = match_type l1 l2 in
      let sr = match_type r1 r2 in
      merge_subst sl sr;
    (~TVar(tv), t) ? kind_equal (kind_tyvar tv) (kind_type t) ->
      single_subst tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 -> null_subst;
    _ -> error "type do not match"
  };

型クラス

type Pred = IsIn (Id, Type);

fun pred_equal p1 p2 =
  match (p1, p2) {
    (~IsIn(id1,t1), ~IsIn(id2,t2)) ->
      id_equal id1 id2 && type_equal t1 t2
  };

fun pred_list_equal ps1 ps2 =
  all (uncurry pred_equal) (zip ps1 ps2);

type Qual<t> = Qual([Pred], t);

fun qual_equal f q1 q2 =
  match (q1, q2) {
    (~Qual(ps1,t1), ~Qual(ps2,t2)) ->
      pred_list_equal ps1 ps2 && f t1 t2
  };

let qual_equal_type =
  qual_equal type_equal;

let apply_pred s = {
  ~IsIn(i,t) -> IsIn(i, apply_type s t)
};

let tv_pred = {
  ~IsIn(i,t) -> tv_type t
};

let apply_pred_list s =
  map (apply_pred s);

let tv_pred_list =
  nub_tyvar_list <<concat_map tv_pred;

let apply_quad_type s = {
  ~Qual(ps,t) -> Qual(apply_pred_list s ps, apply_type s t)
};

let tv_pred_type = {
  ~Qual(ps,t) -> tv_pred_list ps `union_tyvar_list` tv_type t
};

fun mgu_maybe t1 t2 =
  match (t1, t2) {
    (~TAp(l1,r1), ~TAp(l2,r2)) ->
      match (mgu_maybe l1 l2) {
        ~Nothing -> Nothing;
        ~Just(s1) ->
          match (mgu_maybe (apply_type s1 r1) (apply_type s1 r2)) {
            ~Nothing -> Nothing;
            ~Just(s2) ->
              Just <| append_subst s1 s2;
          }
      };
    (~TVar(tv), t) -> Just <| var_bind tv t;
    (t, ~TVar(tv)) -> Just <| var_bind tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 -> Just null_subst;
    _ -> Nothing
  };

fun match_type_maybe t1 t2 =
  match (t1, t2) {
    (~TAp(l1,r1), ~TAp(l2,r2)) ->
      match (match_type_maybe l1 l2) {
        ~Nothing -> Nothing;
        ~Just(sl) ->        
          match (match_type_maybe r1 r2) {
            ~Nothing -> Nothing;
            ~Just(sr) ->
              Just <| merge_subst sl sr
          }              
      };
    (~TVar(tv), t) ? kind_equal (kind_tyvar tv) (kind_type t) ->
      Just <| single_subst tv t;
    (~TCon(tc1), ~TCon(tc2)) ? tycon_equal tc1 tc2 -> Just null_subst;
    _ -> Nothing
  };

let mgu_pred p1 p2 =
  match (p1,p2) {
    (~IsIn(i1,t1), ~IsIn(i2,t2)) ->
      if id_equal i1 i2 -> mgu_maybe t1 t2
      else Nothing
  };

let match_pred p1 p2 =
  match (p1,p2) {
    (~IsIn(i1,t1), ~IsIn(i2,t2)) ->
      if id_equal i1 i2 -> match_type_maybe t1 t2
      else Nothing
  };

type Inst = Inst(Qual<Pred>);

type Class = Class([Id], [Inst]);

type ClassEnv = ClassEnv(Id -> Maybe<Class>, [Type]);

let classes ~ClassEnv(cs, _) = cs;
let defaults ~ClassEnv(_, ts) = ts;

let super ce i =
  match (classes ce i) {
    ~Just(~Class(is, _)) -> is
  };

let insts ce i =
  match (classes ce i) {
    ~Just(~Class(_, its)) -> its
  };

let defined = is_just;

let modify ce i c =
  match ce {
    ~ClassEnv(cs,ts) ->
      let f j = if id_equal i j -> Just c
                else classes ce j in
      ClassEnv(f,ts)
  };

let initial_env =
  ClassEnv(\i -> error "class not defined", [t_integer, t_double]);

type EnvTransformer = EnvTransformer(ClassEnv -> Maybe<ClassEnv>);

let seq ~EnvTransformer(f) ~EnvTransformer(g) =
  EnvTransformer (\ce ->
    match (f ce) {
      ~Nothing -> Nothing;
      ~Just(ce2) -> g ce2
    });

let add_class i is =
  EnvTransformer (\ce ->
    if defined (classes ce i) -> Nothing
    else if any (not << defined << classes ce) is -> Nothing
    else Just (modify ce i (Class(is, []))));

let add_core_classes =
  add_class (Id "Eq") [] `seq`
  add_class (Id "Ord") [Id "Eq"] `seq`
  add_class (Id "Show") [] `seq`
  add_class (Id "Read") [] `seq`
  add_class (Id "Bounded") [] `seq`
  add_class (Id "Enum") [] `seq`
  add_class (Id "Functor") [] `seq`
  add_class (Id "Monad") [];

let add_num_classes =
  add_class (Id "Num") [Id "Eq", Id "Show"] `seq`
  add_class (Id "Real") [Id "Num", Id "Ord"] `seq`
  add_class (Id "Fractional") [Id "Num"] `seq`
  add_class (Id "Integral") [Id "Real", Id "Enum"] `seq`
  add_class (Id "RealFrac") [Id "Real", Id "Fractional"] `seq`
  add_class (Id "Floating") [Id "Fractional"] `seq`
  add_class (Id "RealFloat") [Id "RealFrac", Id "Floating"];

let add_prelude_classes =
  add_core_classes `seq` add_num_classes;

let overlap p q =
  defined (mgu_pred p q);

let add_inst ps (~IsIn(i,_) as p) =
  EnvTransformer (\ce ->
    let its = insts ce i in
    let qs = for ~Inst(~Qual(_, q)) <- its in q in
    let c = Class (super ce i, Inst(Qual(ps, p)) :: its) in
    if not (defined (classes ce i)) -> Nothing
    else if any (overlap p) qs -> Nothing
    else Just (modify ce i c));

let example_insts =
  add_prelude_classes `seq`
  add_inst [] (IsIn(Id "Ord", t_unit)) `seq`
  add_inst [] (IsIn(Id "Ord", t_char)) `seq`
  add_inst [] (IsIn(Id "Ord", t_int)) `seq`
  add_inst [IsIn (Id "Ord", (TVar (Tyvar (Id "a", Star)))),
            IsIn (Id "Ord", (TVar (Tyvar (Id "b", Star))))]
           (IsIn (Id "Ord", (pair (TVar (Tyvar (Id "a", Star)))
                                  (TVar (Tyvar (Id "b", Star))))));

ここまでの感想

• だんだん何のプログラムを書いているのか分からなくなってきた。論文をきちんと読んで復習する必要がある。
• ある程度道具立てがそろってきたので、Mokkosu の機能不足が気にならなくなってきた。

つづく