はじめに

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

前回に引き続き、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です。

つづく。

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

はじめに

7. Type Classes, Predicates and Qualified Types

7.1 Basic Definitions

7.2 Class Environments