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

はじめに

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

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

型クラス (続き)

fun by_super ce (~IsIn(i,t) as p) =
  p :: concat (for i2 <- super ce i in by_super ce (IsIn(i2,t)));

let mplus_maybe m1 m2 =
  match (m1, m2) {
    (~Nothing, ~Nothing) -> Nothing;
    (~Just(x), ~Nothing) -> Just(x);
    (~Nothing, ~Just(x)) -> Just(x);   
    (~Just(x), ~Just(_)) -> Just(x);
  };

fun msum_maybe = {
  [] -> Nothing;
  x :: xs -> x `mplus_maybe` msum_maybe xs
};

let by_inst ce (~IsIn(i,t) as p) =
  let try_inst ~Qual(ps,h) =
    match (match_pred h p) {
      ~Nothing -> Nothing;
      ~Just(u) ->
        Just (map (apply_pred u) ps)
    }
  in
  msum_maybe (for ~Inst(it) <- insts ce i in try_inst it);

fun mem_pred_list p lis =
  match lis {
    [] -> false;
    p1 :: rest -> pred_equal p p1 && mem_pred_list p rest
  };

fun entail ce ps p =
  any (mem_pred_list p) (map (by_super ce) ps) ||
  (match (by_inst ce p) {
     ~Nothing -> false;
     ~Just(qs) -> all (entail ce ps) qs
   });

let in_hnf ~IsIn(_,t) =
  fun hnf = {
    ~TVar(v) -> true;
    ~TCon(tc) -> false;
    ~TAp(t,_) -> hnf t
  } in hnf t;

fun to_hnfs ce ps =
  concat (map (to_hnf ce) ps)

and to_hnf ce p =
  if in_hnf p -> [p]
  else
    match (by_inst ce p) {
      ~Nothing -> error "context resuction";
      ~Just(ps) -> to_hnfs ce ps   
    };

let simplify ce =
  fun loop rs = {
    [] -> rs;
    p :: ps ? entail ce (rs ++ ps) p -> loop rs ps;
    p :: ps -> loop (p :: rs) ps
  }
  in loop [];

let reduce ce ps =
  simplify ce <| to_hnfs ce ps;

let sc_entail ce ps p =
  any (mem_pred_list p) (map (by_super ce) ps);

#------------------------------
# 8. Type Schemes
#------------------------------

type Scheme = Forall ([Kind], Qual<Type>);

let kind_list_equal ks1 ks2 =
  all (uncurry kind_equal) (zip ks1 ks2);

let scheme_euqal sc1 sc2 =
  match (sc1, sc2) {
    (~Forall(ks1,q1), ~Forall(ks2,q2)) ->
      kind_list_equal ks1 ks2 && qual_equal_type q1 q2 
  };

let apply_scheme s ~Forall(ks,qt) =
  Forall(ks, apply_qual_type s qt);

let tv_scheme ~Forall(ks,qt) = tv_qual_type qt;

let quantify vs qt =
  let vs2 = for v <- tv_qual_type qt;
                if mem_tyvar_list v vs in v
  in
  let ks = map kind_tyvar vs2 in
  let s = Subst (zip vs2 (map TGen (0 .. length vs2))) in
  Forall (ks, apply_qual_type s qt);

let to_scheme t =
  Forall([], Qual([], t));

仮定

type Assump = Assump(Id, Scheme);

let apply_assump s ~Assump(i,sc) =
  Assump(i, apply_scheme s sc);

let tv_assump ~Assump(i,sc) = tv_scheme sc;

fun find (~Id(s) as i) = {
  [] -> error <| "unbound identifier: " ^ s;
  ~Assump(i2, sc) :: rest ->
    if id_equal i i2 -> sc
    else find i rest
};

型推論の状態

let subst = ref null_subst;
let count = ref 0;

let get_subst () = !subst;

let ext_subst s2 =
  subst := s2 `append_subst` !subst;

let unify t1 t2 =
  let s = get_subst () in
  let u = mgu (apply_type s t1) (apply_type s t2) in
  ext_subst u;

let new_tvar k =
  let n = !count in
  do incr count in
  TVar (Tyvar (enum_id n, k));

fun inst_type ts = {
  ~TAp(l,r) -> TAp(inst_type ts l, inst_type ts r);
  ~TGen(n) -> nth ts n;
  t -> t
};

let inst_pred ts ~IsIn(c,t) =
  IsIn(c, inst_type ts t);
  
let inst_pred_list ts ps =
  map (inst_pred ts) ps;
  
let inst_qual ts ~Qual(ps,t) =
  Qual(inst_pred_list ts ps, inst_type ts t);


let fresh_inst ~Forall(ks,qt) =
  let ts = map new_tvar ks in
  inst_qual ts qt;

ここまでの感想

• もはや何のプログラムを書いているのか自分でも理解していない。

つづく