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

# はじめに

Simon Peyton Jones 論文 Typing Haskell in Haskell を参考に Haskell の型システムの実装に挑戦しています。実装には関数型言語の [Mokkosu](http://lambdataro.sakura.ne.jp/mokkosu/) を使っています。

* [Mark P Jones: Typing Haskell in Haskell](http://web.cecs.pdx.edu/~mpj/thih/)
* [MokkosuでHaskellの型システムを作る (その1)](http://qiita.com/lambdataro/items/1e4d795d3dd97a94c8f3)
* [MokkosuでHaskellの型システムを作る (その2)](http://qiita.com/lambdataro/items/c19e0d6d637e0dbb52ca)
* [MokkosuでHaskellの型システムを作る (その3)](http://qiita.com/lambdataro/items/681cabee9c307b0d5e3e)
* [MokkosuでHaskellの型システムを作る (その4)](http://qiita.com/lambdataro/items/ffe1544b13b5b5458b4c)
* [MokkosuでHaskellの型システムを作る (その5)](http://qiita.com/lambdataro/items/2018737b9d578600c222)
* [MokkosuでHaskellの型システムを作る (その6)](http://qiita.com/lambdataro/items/e1ba95453ac10c6c308e)

前回に引き続き、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`に変えたバージョンを使うと無駄がなくなります。

つづく