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

はじめに

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)

型推論

type Literal = LitInt(Int)
             | LitChar(Char)
             | LitRat(Double)
             | LitStr(String)
;

let ti_lit = {
  ~LitChar(_) -> ([], t_char);
  ~LitInt(_) ->
    let v = new_tvar Star in
    ([IsIn(Id "Num", v)], v);
  ~LitStr(_) -> ([], t_string);
  ~LitRat(_) ->
    let v = new_tvar Star in
    ([IsIn(Id "Fractional", v)], v)
};

type Pat = PVar(Id)
         | PWildcard
         | PAs(Id, Pat)
         | PLit(Literal)
         | PNpk(Id, Int)
         | PCon(Assump, [Pat]);

fun ti_pat = {
  ~PVar(i) ->
    let v = new_tvar Star in
    ([], [Assump(i, to_scheme v)], v);
  ~PWildcard ->
    let v = new_tvar Star in
    ([], [], v);
  ~PAs(i, p) ->
    let (ps, a, t) = ti_pat p in
    (ps, Assump(i, to_scheme t) :: a, t);
  ~PLit(l) ->
    let (ps, t) = ti_lit l in
    (ps, [], t);
  ~PNpk(i,k) ->
    let t = new_tvar Star in
    ([IsIn(Id "Integral", t)], [Assump(i, to_scheme t)], t);
  ~PCon(~Assump(i, sc), pats) ->
    let (ps, a, ts) = ti_pats pats in
    let t2 = new_tvar Star in
    let ~Qual(qs,t) = fresh_inst sc in
    do unify t (foldr fn t2 ts) in
    (ps ++ qs, a, t2)
}
and ti_pats pats =
  let psasts = map ti_pat pats in
  let ps = concat (for (qs2, _, _) <- psasts in qs2) in
  let a  = concat (for (_, a2, _)  <- psasts in a2 ) in
  let ts = for (_, _, t) <- psasts in t in
  (ps, a, ts)
;

type Expr = Var(Id)
          | Lit(Literal)
          | Const(Assump)
          | Ap(Expr, Expr)
          | Let(BindGroup, Expr)

and Alt = Alt([Pat], Expr)

and Impl = Impl(Id, [Alt])

and BindGroup = BindGroup([Expl], [[Impl]])

and Ambiguity = Ambiguity(Tyvar, [Pred])

and Expl = Expl(Id, Scheme, [Alt]);

fun diff_pred_list ps1 ps2 =
  match ps1 {
    [] -> [];
    p :: ps ->
      if mem_pred_list p ps2 ->
        diff_pred_list ps ps2
      else
        p :: diff_pred_list ps ps2
  };

fun diff_tyvar_list tvs1 tvs2 =
  match tvs1 {
    [] -> [];
    tv :: tvs ->
      if mem_tyvar_list tv tvs2 ->
        diff_tyvar_list tvs tvs2
      else
        tv :: diff_tyvar_list tvs tvs2
  };

let num_classes = [
  Id "Num", Id "Integral", Id "Floating", Id "Fractional",
  Id "Real", Id "RealFloat", Id "RealFrac"
];

let std_classes = [
  Id "Eq", Id "Ord", Id "Show", Id "Read", Id "Bounded", Id "Enum",
  Id "Ix", Id "Functor", Id "Monad", Id "MonadPlus"
] ++ num_classes;

let apply_assump_list s =
  map (apply_assump s);

let tv_assump_list a =
  nub_tyvar_list <| concat_map tv_assump a;

let foldl1 f lis = foldl f (head lis) (tail lis);

fun ti_expr ce a = {
  ~Var(i) ->
    let sc = find i a in
    let ~Qual(ps,t) = fresh_inst sc in
    (ps, t);
  ~Const(~Assump(i,sc)) ->
    let ~Qual(ps,t) = fresh_inst sc in
    (ps, t);
  ~Lit(l) ->
    ti_lit l;
  ~Ap(e,f) ->
    let (ps, te) = ti_expr ce a e in
    let (qs, tf) = ti_expr ce a f in
    let t = new_tvar Star in
    do unify (tf `fn` t) te in
    (ps ++ qs, t);
  ~Let(bg,e) ->
    let (ps, a2) = ti_bind_group ce a bg in
    let (qs, t) = ti_expr ce (a2 ++ a) e in
    (ps ++ qs, t)
}

and ti_alt ce a ~Alt(pats,e) =
  let (ps,a2,ts) = ti_pats pats in
  let (qs,t) = ti_expr ce (a2 ++ a) e in
  (ps ++ qs, foldl fn t ts)

and ti_alts ce a alts t =
  let psts = map (ti_alt ce a) alts in
  do iter (unify t) (map snd psts) in
  concat (map fst psts)

and split ce fs gs ps =
  let ps2 = reduce ce ps in
  let (ds, rs) = partition (all (flip elem fs) << tv_pred) ps2 in
  let rs2 = defaulted_preds ce (fs ++ gs) rs in
  (ds, diff_pred_list rs rs2)

and ambiguities ce vs ps =
  for v <- tv_pred_list ps `diff_tyvar_list` vs in
    Ambiguity (v, filter (elem v << tv_pred) ps)

and candidates ce ~Ambiguity(v, qs) =
  let is = for ~IsIn(i,t) <- qs in i in
  let ts = for ~IsIn(i,t) <- qs in t in
  for if all (type_equal (TVar v)) ts;
      if any (flip elem num_classes) is;
      if all (flip elem std_classes) is;
      t2 <- defaults ce;
      if all (entail ce []) (for i <- is in IsIn(i,t2))
  in t2

and with_defaults f ce vs ps =
  let vps = ambiguities ce vs ps in
  let tss = map (candidates ce) vps in
  if any is_nil tss -> error "cannot resolve ambiguity"
  else f vps (map head tss)

and defaulted_preds ce =
  with_defaults (\vps ts -> concat_map (\~Ambiguity(_,x) -> x) vps) ce

and with_defaults2 f ce vs ps =
  let vps = ambiguities ce vs ps in
  let tss = map (candidates ce) vps in
  if any is_nil tss -> error "cannot resolve ambiguity"
  else f vps (map head tss)

and default_subst ce tvs ps =
  with_defaults2 (\vps ts -> zip (map (\~Ambiguity(x,_) -> x) vps) ts)
    ce tvs ps |> Subst

and ti_expl ce a ~Expl(i,sc,alts) =
  let ~Qual(qs,t) = fresh_inst sc in
  let ps = ti_alts ce a alts t in
  let s = get_subst () in
  let qs2 = apply_pred_list s qs in
  let t2 = apply_type s t in
  let fs = tv_assump_list (apply_assump_list s a) in
  let gs = tv_type t2 `diff_tyvar_list` fs in
  let sc2 = quantify gs (Qual (qs2, t2)) in
  let ps2 = filter (not << entail ce qs2) (apply_pred_list s ps) in
  let (ds, rs) = split ce fs gs ps2 in
  if not (scheme_equal sc sc2) ->
    error "signature too general"
  else if not (is_nil rs) ->
    error "context too weak"
  else
    ds

and restricted bs =
  let simple ~Impl(i,alts) = any (\~Alt(x,_) -> is_nil x) alts in
  any simple bs

and ti_impls ce a bs =
  let ts = map (\_ -> new_tvar Star) bs in
  let is = map (\~Impl(x,_) -> x) bs in
  let scs = map to_scheme ts in
  let a2 = zip_with (curry Assump) is scs ++ a in
  let altss = map (\~Impl(_,y) -> y) bs in
  let pss = zip_with (ti_alts ce a2) altss ts in
  let s = get_subst () in
  let ps2 = apply_pred_list s (concat pss) in
  let ts2 = apply_type_list s ts in
  let fs = tv_assump_list (apply_assump_list s a) in
  let vss = map tv_type ts2 in
  let gs = foldl1 union_tyvar_list vss `diff_tyvar_list` fs in
  let (ds,rs) = split ce fs (foldl1 intersect_tyvar_list vss) ps2 in
  if restricted bs ->
    let gs2 = gs `diff_tyvar_list` tv_pred_list rs in
    let scs2 = map (\x -> quantify gs2 (Qual([], x))) ts2 in
    (ds ++ rs, zip_with (curry Assump) is scs2)
  else
    let scs2 = map (\x -> quantify gs (Qual (rs, x))) ts2 in
    (ds, zip_with (curry Assump) is scs2)

and ti_bind_group ce a ~BindGroup(es,iss) =
  let a2 = for ~Expl(v,sc,alts) <- es in Assump(v,sc) in
  let (ps, a3) = ti_seq ti_impls ce (a2 ++ a) iss in
  let qss = map (ti_expl ce (a3 ++ a2 ++ a)) es in
  (ps ++ concat qss, a3 ++ a2)

and ti_seq ti ce a = {
  [] -> ([], []);
  bs :: bss ->
    let (ps, a2) = ti ce a bs in
    let (qs, a3) = ti_seq ti ce (a2 ++ a) bss in
    (ps ++ qs, a3 ++ a2)
}

and ti_seq2 ti ce a = {
  [] -> ([], []);
  bs :: bss ->
    let (ps, a2) = ti ce a bs in
    let (qs, a3) = ti_seq2 ti ce (a2 ++ a) bss in
    (ps ++ qs, a3 ++ a2)
};


type Program = Program([BindGroup]);

let ti_program ce (a : [Assump]) ~Program(bgs) =
  do init_state () in
  let (ps, a2) = ti_seq2 ti_bind_group ce a bgs in
  let s = get_subst () in
  let rs = reduce ce (apply_pred_list s ps) in
  let s2 = default_subst ce [] rs in
  apply_assump_list (s2 `append_subst` s) a2;

ここまでの感想

• プログラムは作り終えた。型も通った。意味は分かっていない。
• 次回は何かサンプルプログラム的なものを動かしてみたいと思う。
• 論文には実行例は載っていないので自力で作る必要がある。

つづく