はじめに

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

前回に引き続き、Haskellから移植したMokkosuコードを解読していきます。

7. Type Classes, Predicates and Qualified Types

7.3 Entailment

述語pと述語のリストpsが与えられた時に、ps内のすべての述語が成立する場合、p`が成立するかどうかを判定する処理をentailmentとよびます
ここで述語とはPred型の値IsIn(id,typ)のことです。 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); }; mplus_maybe : Maybe<α> -> Maybe<α> -> Maybe<α>
mplus_maybeは2つのMaybe型の値に関する足し算の定義です。

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

msum_maybe : [Maybe<α>] -> Maybe<α>

msum_maybeはMaybe型の値を左から順に足していく関数です。

fun pred_list_elem p = {
  [] -> false;
  p2 :: rest -> pred_equal p p2 && pred_list_elem p rest
};

pred_list_elem : Pred -> [Pred] -> Bool

Pred型の値のリストに対するelem関数です。

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

by_super : ClassEnv -> Pred -> [Pred]

by_super関数はクラス環境から述語のすべてのスーパークラスを求めるです。
スーパークラスの結果には自分自身も含めています。
結果は重複を含む可能性がありますが、クラス階層に循環は無いので有限長になります。

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

by_inst : ClassEnv -> Pred -> Maybe<[Pred]>

クラス環境ce内のiという名前のクラスのすべてのインスタンス宣言について、try_inst関数を試し、最初にJustを返したものを返します。
try_inst関数では、述語hと述語pのマッチングを行い、マッチした場合Justを返します。
Justの場合、判定する必要のある残りの述語を返します。このとき、マッチした場合の代入を各述語に適用しておきます。
Haskellはインスタンスの重複を許さないので、マッチするものは存在する場合は高々一つになります。

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

entail : ClassEnv -> [Pred] -> Pred -> Bool

entail関数は、クラス環境と述語のリスト、述語を受け取り、述語のリストが成立すると仮定して、述語が成立するかを判定する関数です。
まず、述語のリストの各述語のスーパークラス内に述語が含まれているかを判定します。
含まれている場合はtrueを返します。
そうでない場合は、クラス環境中に述語にマッチするインスタンス宣言があるかどうかを探します。
見つからない場合はfalseを返します。
見つかった場合は、そのインスタンス宣言の仮定について、それらが成立するかを再帰的に判定します。

7.4 Context Recution

述語のリストをよりシンプルなものに変換する操作をコンテキストリダクションとよぶ。

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

in_hnf : Pred -> Bool

型がhnf (head normal form) の形をしているかを判定する。
hnfはv t1 t2 ...という形式。ここでvは型変数、tnは型。
Haskellではクラスの引数は構文上hnfである必要がある。

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 reduction";
      ~Just(ps) -> to_hnfs ce ps
    };

to_hnfs : ClassEnv -> [Pred] -> [Pred]
to_hnf : ClassEnv -> Pred -> [Pred]

to_hnf関数は述語pがhnf形式になりまで、by_inst関数を使って簡約操作を行います。

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 [];

simplify : ClassEnv -> [Pred] -> [Pred]

simplify関数は述語のリストを単純化します。
単純化には先に定義したentail関数を使っています。
p :: psのとき、psの定義が成り立つと仮定したとき、pが成り立つとき、pは不要な定義なので削除します。
そうでないときは、必要な定義なので返すリストに追加します。

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

reduce : ClassEnv -> [Pred] -> [Pred]

reduce関数は、述語のリストをhnf形式に変換して単純化します。

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

sc_entail : ClassEnv -> [Pred] -> Pred -> Bool

entail関数のorの条件の前半部分だけのバージョンです。
reduce関数では、simplifyに渡す前に述語がhnfになっていることが保証されています。
hnf形式の述語はHaskellの構文の制限に従ったインスタンス宣言にマッチすることはありません。
ここでHaskellの構文の制限とは、インスタンス宣言に型変数が含まれてはいけない制限のことだと思われます。
そこでsimplifyのentailをこのsc_entailに変えたバージョンを使うと無駄がなくなります。

つづく

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

はじめに

7. Type Classes, Predicates and Qualified Types

7.3 Entailment

7.4 Context Recution