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

# はじめに

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)

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

# 7. Type Classes, Predicates and Qualified Types
## 7.1 Basic Definitions
```
type Pred = IsIn (String, Type);
```
* `Pred(id, t)`で型`t`が`id`という名前の型クラスのメンバであることを示します。

```
fun pred_equal ~IsIn(id1, t1) ~IsIn(id2, t2) =
  id1 == id2 && type_equal t1 t2;
```
```
pred_equal : Pred -> Pred -> Bool
```
* `pred_equal`は与えられた2つの`Pred`型の値が等しいかどうかを検査します。

```
fun pred_list_equal ps1 ps2 =
  length ps1 == length ps2 &&
  all (uncurry pred_equal) (zip ps1 ps2);
```
```
pred_list_equal : [Pred] -> [Pred] -> Bool
```
* `pred_list_equal`は`Pred`型の値の列が等しいかどうかを検査します。

```
type Qual<T> = Qual([Pred], T);
```
* `Qual`は型クラスで修飾された値を表します。

```
fun qual_equal f ~Qual(ps1,v1) ~Qual(ps2,v2) =
  pred_list_equal ps1 ps2 && f v1 v2;
```
```
qual_equal : (α -> β -> Bool) -> Qual<α> -> Qual<β> -> Bool
```
* `qual_equal`は2つの`Qual`の等しさを調べる関数です。
* 第1引数には`Qual`の2要素目の等しさを調べる関数を与えます。

```
let qual_type_equal = qual_equal type_equal;
```
```
qual_type_equal : Qual<Type> -> Qual<Type> -> Bool
```
* `qual_type_equal`は型クラスで修飾された型の等しさを調べる関数です。

```
let pred_apply s ~IsIn(i,t) =
  IsIn(i, type_apply s t);
```
```
pred_apply : Subst -> Pred -> Pred
```
* `Pred`型の型部分に代入を適用します。

```
let pred_list_apply s =
  map (pred_apply s);
```
```
pred_list_apply : Subst -> [Pred] -> [Pred]
```
* `Pred`型の値のリストに代入を適用します。

```
let qual_type_apply s ~Qual(ps,t) =
  Qual (pred_list_apply s ps, type_apply s t);
```
```
qual_type_apply : Subst -> Qual<Type> -> Qual<Type>
```
* 型クラスで修飾された型に対して代入を適用します。

```
let pred_tv ~IsIn(i,t) =
  type_tv t;
```
```
pred_tv : Pred -> [Tyvar]
```
* `Pred`型の値に含まれる型変数の集合を返します。

```
let pred_list_tv =
  tyvar_list_nub << concat_map pred_tv;
```
```
pred_list_tv : [Pred] -> [Tyvar]
```
* `Pred`型の値のリストに含まれる型変数の集合を返します。

```
let qual_type_tv ~Qual(ps,t) =
  pred_list_tv ps `tyvar_list_union` type_tv t;
```
```
qual_type_tv : Qual<Type> -> [Tyvar]
```
* 型クラスで修飾された型に含まれる型変数の集合を返します。

```
let mgu_maybe t1 t2 =
  try (Just (mgu t1 t2), const Nothing);
```
```
mgu_maybe : Type -> Type -> Maybe<Subst>
```
* エラーの際に`Nothing`を返す`mgu`関数です。

```
let pred_mgu ~IsIn(i1,t1) ~IsIn(i2,t2) =
  if i1 == i2 -> mgu_maybe t1 t2
  else Nothing;
```
```
pred_mgu : Pred -> Pred -> Maybe<Subst>
```
* `Pred`型の値に対する`mgu`関数です。

```
let type_match_maybe t1 t2 =
  try (Just (type_match t1 t2), const Nothing);
```
```
type_match_maybe : Type -> Type -> Maybe<Subst>
```
* エラーの際に`Nothing`を返す`type_match`関数です。

```
let pred_match ~IsIn(i1,t1) ~IsIn(i2,t2) =
  if i1 == i2 -> type_match_maybe t1 t2
  else Nothing;
```
```
pred_match : Pred -> Pred -> Maybe<Subst>
```
* `Pred`型の値に対する`match`関数です。

```
type Inst = Inst(Qual<Pred>);
```
* `Inst`はインスタンス宣言を表す値の型です。

```
type Class = Class([String], [Inst]);
```
* `Class`はスーパークラスとインスタンス宣言の組で表現します。

## 7.2 Class Environments

```
type ClassEnv = ClassEnv(String -> Maybe<Class>, [Type]);
```
* クラス環境とはクラス宣言とインスタンス宣言の情報と、型が曖昧になったときのデフォルトの型指定から構成されます。

```
let classes ~ClassEnv(cs, _) = cs;
```
```
classes : ClassEnv -> String -> Maybe<Class>
```
* クラス環境からクラスを探索する関数を取り出す関数です。

```
let defaults ~ClassEnv(_, defs) = defs;
```
```
defaults : ClassEnv -> [Type]
```
* クラス環境からデフォルトの型のリストを取り出す関数です。

```
let super ce i =
  match (classes ce i) {
    ~Just(~Class(is, _)) -> is;  
  };
```
```
super : ClassEnv -> String -> [String]
```
* `super`関数はクラス環境とクラス名から、そのクラスのスーパークラスの名前のリストを返します。

```
let insts ce i =
  match (classes ce i) {
    ~Just(~Class(_, its)) -> its
  };
```
```
insts : ClassEnv -> String -> [Inst]
```
* `insts`関数はクラス環境とクラス名から、そのクラスのインスタンス宣言のリストを返します。

```
let defined = is_just;
```
```
defined : Maybe<α> -> Bool
```
* `defined`関数は値が定義されているかどうかを判定するのに使います。

```
let modify ~ClassEnv(cs,defs) id c =
  let f id2 = if id == id2 -> Just c else cs id2 in
  ClassEnv (f, defs);
```
```
modify : ClassEnv -> String -> Class -> ClassEnv
```
* `modify`関数はクラス環境に指定した名前でクラスを登録します。

```
let initial_env =
  ClassEnv (\i -> error "class not defined", [t_integer, t_double]);
```
```
initial_env : ClassEnv
```
* `initial_env`は空のクラス環境です。

```
type EnvTransformer = EnvTransformer(ClassEnv -> Maybe<ClassEnv>);
```
* `EnvTransformer`は既存のクラス環境を受け取って、それになんらかのクラスを追加する関数です。
* 追加する際に既存の定義と整合性がとれているかの検査を行います。

```
let seq ~EnvTransformer(f) ~EnvTransformer(g) =
  EnvTransformer (\ce ->
    match (f ce) {
      ~Nothing -> Nothing;
      ~Just(ce2) -> g ce2
    });
```
```
seq : EnvTransformer -> EnvTransformer -> EnvTransformer
```
* `seq`関数は2つの`EnvTransformer`を連結します。

```
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, []))));
```
```
add_class : String -> [String] -> EnvTransformer
```
* `add_class`関数はクラスを追加する`EnvTransformer`を作る関数です。
* 引数はクラス名とスーパークラスの名前のリストです。
* クラスが既に定義済みでないこと、すべてのスーパークラスが定義済みであることを検査するコードが含まれています。

```
let add_core_classes =
  add_class "Eq" [] `seq`
  add_class "Ord" ["Eq"] `seq`
  add_class "Show" [] `seq`
  add_class "Read" [] `seq`
  add_class "Bounded" [] `seq`
  add_class "Enum" [] `seq`
  add_class "Functor" [] `seq`
  add_class "Monad" [];
```
```
add_core_classes : EnvTransformer
```
* コアクラスの`EnvTransformer`。

```
let add_num_classes =
  add_class "Num" ["Eq", "Show"] `seq`
  add_class "Real" ["Num", "Ord"] `seq`
  add_class "Fractional" ["Num"] `seq`
  add_class "Integral" ["Real", "Enum"] `seq`
  add_class "RealFrac" ["Real", "Fractional"] `seq`
  add_class "Floating" ["Fractional"] `seq`
  add_class "RealFloat" ["RealFrac", "Floating"];
```
```
add_num_classes : EnvTransformer
```
* 数値クラスの`EnvTransformer`。

```
let add_prelude_classes =
  add_core_classes `seq` add_num_classes;
```
```
add_prelude_classes : EnvTransformer
```
* 標準プレリュードの`EnvTransformer`。

```
let overlap p q =
  defined (pred_mgu p q);
```
```
overlap : Pred -> Pred -> Bool
```
* `overlap`関数は2つの述語が等しいかもしくは等しくできる可能性があるかを検査します。

```
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));
```
```
add_inst : [Pred] -> Pred -> EnvTransformer
```
* `add_inst`関数はインスタンス宣言を追加する`EnvTransformer`を作る関数です。
* 1引数目はインスタンス宣言の前提部分、2引数目がインスタンス宣言の本体です。
* `add_inst`の実装ではまず、既に定義されているインスタンス宣言を探してきます。
* インスタンス宣言は`Qual<Pred>`型で表していたことを思い出してください。
* この`Pred`部分を集めてきた変数が`qs`です。
* `c`は今回更新する新しい`Class`型の値です。
* もし、`i`という名前のクラスが既に存在すれば失敗します。
* また、オーバーラップするインスタンス宣言がすでに存在する場合も失敗します。
* そうでない場合は、クラス環境の定義を更新したものを返します。

```
let example_insts =
  add_prelude_classes `seq`
  add_inst [] (IsIn("Ord", t_unit)) `seq`
  add_inst [] (IsIn("Ord", t_char)) `seq`
  add_inst [] (IsIn("Ord", t_int)) `seq`
  add_inst [IsIn ("Ord", (TVar (Tyvar ("a", Star)))),
            IsIn ("Ord", (TVar (Tyvar ("b", Star))))]
           (IsIn ("Ord", (pair (TVar (Tyvar ("a", Star)))
                               (TVar (Tyvar ("b", Star))))));
```
```
example_insts : EnvTransformer
```
* 標準プレリュードに加え、`Ord`クラスのインスタンス宣言を加えます。`EnvTransformer`です。

つづく。