概要
Prologによって型クラスを１６０行で作りました。また、分かりやすく型クラスの実装方法を説明します。
はじめに
型クラスは Haskell や Scala などの言語を構築する上で非常に重要な機能の一つで、アドホックな多相的な関数オーバーロードを実装するための仕組みです。ここでは、まずとても短い型クラスの実装を見ていただき、より小さな型クラスの実装を目指した論文に注目していくつかの型クラスの論文を紹介します。
実装
ではPrologによるパラメトリック型クラスの実装を見ていきましょう。
まずは以下のコードをご覧ください:
:- tpp(
type Colour = 'MkColour'!(int,int,int);
type Point = 'MkPoint'!(float,float);
type CPoint = 'MkCPoint'!(float,float,Colour);
val 'MkColour' : (int->int->int->Colour);
val c1 : (Colour->int);
val c2 : (Colour->int);
val c3 : (Colour->int);
val 'MkPoint' : (float->float->Point);
val pt1 : (Point->float);
val pt2 : (Point->float);
val 'MkCPoint' : (float->float->Colour->CPoint);
val cpt1 : (CPoint->float);
val cpt2 : (CPoint->float);
val cpt3 : (CPoint->colour);
val add : (float->float->float);
val sqr : (float->float);
val sqrt : (float->float);
class P:XCoord where xcoord:(P->float);
class P2:YCoord where ycoord:(P2->float);
inst Point:XCoord where xcoord=λ(u,pt1$u);
inst Point:YCoord where ycoord=λ(u,pt2$u);
inst CPoint:XCoord where xcoord=λ(u,cpt1$u);
inst CPoint:YCoord where ycoord=λ(u,cpt2$u);
let distance=λ(p,sqrt$(add$(sqr$(xcoord$p))$(sqr$(ycoord$p))));
distance$('MkCPoint'$2.0$3.0$('MkColour'$0$0$0))
,R),!,R==float.
:- halt.
このプログラムはPrologのコードですが、型クラスを実装した言語での型検査をするプログラムです。
typeは型定義、valは変数の型定義、classが型クラスを定義し、instが型クラスのインスタンスを宣言し、
letはlet式を表します。λ(x,e) がラムダ抽象で、e $ e は関数適用を表します。
この型検査、tppの実装を以下に示します:
:- module(param,
[foldr/4,fv/2,gfv/2,cfv/2,cdom/2,capp/3,creg/2,gfv/2, tpgen/5,put/2,get/2,tp1/2,tp3/3, tpp/2]).
:- expects_dialect(sicstus).
:- op(500,xfx,!).
:- op(600,yfx,[∈, ⊑ , ˄, $]).
:- op(700,xfy,[=>,where]).
:- op(900,xfx,ⱶo).
:- op(1200, xfx, --).
:- op(990,fy,[let,inst,val,class,type]).
:- set_prolog_flag(occurs_check, true).
term_expansion((A--B), (B:-A)).
member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).
union_eq([],Ys,Ys) :- !.
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!, union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).
subtract_eq([],_,[]) :- !.
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!,subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).
del_eq(C,A,C_) :- foldr(del_eq1(A),C,[],C_).
del_eq1(A,(B,_),F,F) :- B==A.
del_eq1(_,(B,V),F,[(B,V)|F]).
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す
walk(F,X,I,R) :- call(F,X,I,R).
walk(F,X,I,R) :- compound(X), X =.. [_|Xs],!,foldl(walk(F),Xs,I,R),!.
walk(_,_,I,I) :- !.
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
% 型の置換
sub(X1/T,X,T) :- X1==X,!.
sub(X1/T,∀(X,Πa,T), ∀(X,Πa,T)) :- X1==X,!.
sub(AB,X,R) :- compound(X),X=..Xs,!,maplist(sub(AB),Xs,R_),R=..R_,!.
sub(_,I,I) :- !.
gsub(S,Γ,Γ_) :- maplist(ysub(S),Γ,Γ_),!. % 型環境の置換
ysub(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.
csub(S,C,C_) :- maplist(csub1(S),C,C_),!.
csub1(S,(A,Γ),(A_,Γ_)) :- !,sub(S,A,A_),gsub(S,Γ,Γ_),!.
% 自由型変数取得
fv(X,R) :- walk(fv1,X,[],R),!. % 自由型変数取得
fv1(X,I,R) :- var(X), union_eq(I,[X],R).
fv1(∀(X,G,T),I,R) :- !,fv(T,Ts),gfv(G,Ts2), union_eq(Ts2,Ts,Ts3),
subtract_eq(Ts3,[X],R1), union_eq(I,R1,R).
gfv(Γ,Xs) :- foldr(gfv1, Γ, [], Xs).% 型環境置換
gfv1((_,T), Fv1,R) :- fv(T,T_),union_eq(Fv1,T_,R).%todo
cfv(C,R) :- maplist(cfv1,C,R1),foldr(union_eq,R1,[],R).
cfv1((_,G),R) :- gfv(G,R).
cdom(C,R) :- maplist(cdom1,C,R). % ドメイン
cdom1((A,_),A).
creg(C,R) :- cdom(C,R1), foldr(creg1(C),R1,[],R). % リージョン(領域)
creg1(C,A,R1,R) :- capp(C,A,G), gfv(G,R2), union_eq(R1,R2,R).
capp(C,A,R) :- (A1,R) ∈ C,A1==A,!. % 適用
capp(_,_,[]).
% 一般化 : 制約Cを一般化できたら環境から回収して清潔さを保つのがポイント
mem(F,A) :- call(F,As),!, A ∈ As. % 述語を実行してメンバ取り出し
memeq(F,A) :- call(F,As),!, member_eq(A,As). % 述語を実行してメンバ判定
tpgen(T,G,C,C_,R) :- mem(cdom(C),A), % CのドメインにあるAで
\+memeq(gfv(G),A), % 環境の自由変数になく
\+memeq(creg(C),A), % リージョン領域にもない
\+memeq(cdom(C_),A), % 元のドメインにもない
capp(C,A,Ca),!, % 制約をとりだし
%(memeq(gfv(Ca),A) ; memeq(fv(T),A)),!, % 追加条件
del_eq(C,A,C2),% 制約リストからAを除外
tpgen(∀(A, Ca, T), G, C2, C_,R).
tpgen(T,_,C,_,(T,C)).
% 具体化
inst(T,C,(T,C)) :- var(T),!;T\= ∀(_,_,_),!. % ∀でなければそのまま
inst(∀(A,G,T),C,R) :- sub(A/B,T,T_),inst(T_,[(B,G)|C],R).% 新しいBで置換、制約追加
% 単一化
mgu(_, T1,T2,C,C) :- T1==T2,!. % 同じ
mgu(G,A,T,C,R) :- var(A),!,mgu1(G,A,T,C,R).% 型変数なら単一化
mgu(G,T,A,C,R) :- var(A),!,mgu1(G,A,T,C,R).
mgu(G,K!T,K!T_,C,R) :- !,mgu(G,T,T_,C,R).% データ引数で単一化
mgu(G,(T1,T2),(T1_,T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%ペア
mgu(G,(T1->T2),(T1_->T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%関数
mgu(_,[],[],C,C) :- !.% ユニット
mgu(_,T1,T2,(_,_),_) :- failwith('mgu error ~w ~w', [T1,T2]).
mgu1(G,A,T,C,R) :- capp(C,A,G1), del_eq(C,A,C2),% 変数制約取得、制約の回収※1
A=T, mgn(G,(A,G1),C2,R),!.% 単一化、回収制約正規化
mgu1(_,A,T,_,_) :- failwith('mgu1 error ~w ~w',[A,T]).
% 正規化アルゴリズム
mgn(G,(A,G1),C,R) :- foldl(mgn1(G,A),G1,C,R). % 制約G1でループ
mgn1(G,A,(D,T),C,R) :- var(A),capp(C,A,G1),!,% 変数なら制約取得
((D_,T_)∈G1,D==D_,!,mgu(G,T,T_,C,R) % クラス有り、単一化
; R=[(A,[(D,T)|G1])|C]).% クラス無し、制約追加(※1戻す)
mgn1(G,K!KT,(D,T),C,R) :- !,(inst C_=>K_!KT_:D_!T_)∈G,K_==K,D_==D,% データ実装検索
!,sub(KT_/KT,T_,T2_),mgu(G,T,T2_,C,C2),% クラス引数単一化
csub(KT_/KT,C_,C2_),% 制約を置換して実体化
foldr(mgn(G),C2_,C2,R).% 実体化した制約で正規化ループ
mgn1(G,(T1,T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% ペア
mgn1(G,(T1->T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% 関数
mgn1(_,[],_,C, C). % ユニット
mgn1(G,T1,Y,C,_) :- failwith('error:~w',[mgn1(G,T1,Y,C)]).
% 型推論(式)
tp(I,_,C,(int,C)) :- integer(I),!.
tp(F,_,C,(float,C)) :- float(F),!.
tp([],_,C,([],C)). :- !. % unit
tp(λ(X,E),G,C,((A->T1),C1)) :- !,tp(E,[(X,A)|G],[(A,[])|C],(T1,C1)).
tp((let X=E1;E2),G,C,R) :- !,tp(E1,G,C,(T1,C1)),tpgen(T1,G,C1,C,(T,C2)),
tp(E2,[(X,T)|G],C2,R).
tp(X,G,C,R) :- atom(X),!,(X,T) ∈ G, inst(T,C,R).
tp((E1$E2),G,C,(A,C3)) :- !,tp(E1,G,C,(T1,C1)),!,tp(E2,G,C1,(T2,C2)),!,
mgu(G,T1,(T2->A),([(A,[])|C2]),C3),!.
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
このように非常に短く型クラスの型検査が実装できます。
そう！型クラスの実装はそんなに難しいものではありません。
このアルゴリズムのポイント
通常のHM型推論に加えて型クラスを追加します。
型に対する制約は常に持ち回る制約環境Cに格納します。
ただし、この制約環境はできるだけ小さく保ちます。
例えば、letによって一般化されるときにはスコープが終わるので制約は型に格納し他で使わないので制約環境から回収します。
単一化で型変数に対する制約も制約環境から回収し正規化処理を行います。
ただし、単一化で回収された制約は正規化時に制約環境に戻されることもあります。
正規化処理ではインスタンス宣言から制約を制約環境に追加することがあります。
class宣言やinst宣言による制約環境への制約の追加はありません。
一般化処理では以前の制約環境に含まれていた制約を型情報に追加はしません。新たに作成された制約だけ追加します。
実装の詳細
それでは、より詳細に Prolog の実装を見ていきましょう。
:- module(param,
[foldr/4,fv/2,gfv/2,cfv/2,cdom/2,capp/3,creg/2,gfv/2, tpgen/5,put/2,get/2,tp1/2,tp3/3, tpp/2]).
module は、 Prolog のプログラムからエクスポートする述語を指定します。
:- expects_dialect(sicstus).
SICS Prologと互換のあるモードに設定します。
:- op(500,xfx,!).
:- op(600,yfx,[∈, ⊑ , ˄, $]).
:- op(700,xfy,[=>,where]).
:- op(900,xfx,ⱶo).
:- op(1200, xfx, --).
:- op(990,fy,[let,inst,val,class,type]).
:- set_prolog_flag(occurs_check, true).
様々な、演算子の指定と、出現検査をするように設定します。
term_expansion((A--B), (B:-A)).
自然演繹スタイルに書くためのマクロです。
member_eq(X,[Y|_]) :- X == Y.
member_eq(X,[_|Xs]) :- member_eq(X,Xs).
同一な変数のリスト内検査です。
union_eq([],Ys,Ys) :- !.
union_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!, union_eq(Xs,Ys,Zs).
union_eq([X|Xs],Ys,[X|Zs]) :- union_eq(Xs,Ys,Zs).
同一変数での集合の和を計算します。
subtract_eq([],_,[]) :- !.
subtract_eq([X|Xs],Ys,Zs) :- member_eq(X,Ys),!,subtract_eq(Xs,Ys,Zs).
subtract_eq([X|Xs],Ys,[X|Zs]) :- subtract_eq(Xs,Ys,Zs).
同一な変数での集合の差を計算します。
del_eq(C,A,C_) :- foldr(del_eq1(A),C,[],C_).
del_eq1(A,(B,_),F,F) :- B==A.
del_eq1(_,(B,V),F,[(B,V)|F]).
同一変数検査でリストから削除します。
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
fold right です。
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す
要素を検査する演算子の定義です。Prologなのでリストから取り出して条件指定して駄目だった場合は次のデータを取り出すといったことに使います。
walk(F,X,I,R) :- call(F,X,I,R).
walk(F,X,I,R) :- compound(X), X =.. [_|Xs],!,foldl(walk(F),Xs,I,R),!.
walk(_,_,I,I) :- !.
Prolog のデータ構造をループで走査し、第一引数の述語を呼び出して成功すればそのまま戻り、失敗した場合は子のノードがあれば再帰的に走査します。
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
エラー時の処理です。OCamlにあわせた感じです。エラー出力したあと死にます。これはもうちょっと改良できそうです。
% 型の置換
sub(X1/T,X,T) :- X1==X,!.
sub(X1/T,∀(X,Πa,T), ∀(X,Πa,T)) :- X1==X,!.
sub(AB,X,R) :- compound(X),X=..Xs,!,maplist(sub(AB),Xs,R_),R=..R_,!.
sub(_,I,I) :- !.
gsub(S,Γ,Γ_) :- maplist(ysub(S),Γ,Γ_),!. % 型環境の置換
ysub(S,(X,T),(X,T_)) :- !,sub(S,T,T_),!.
csub(S,C,C_) :- maplist(csub1(S),C,C_),!.
csub1(S,(A,Γ),(A_,Γ_)) :- !,sub(S,A,A_),gsub(S,Γ,Γ_),!.
置換の処理をします。subが式の置換で、gsubが型環境の置換、ysubが型環境の要素１つの処理 csubは制約の置換処理です。
% 自由型変数取得
fv(X,R) :- walk(fv1,X,[],R),!. % 自由型変数取得
fv1(X,I,R) :- var(X), union_eq(I,[X],R).
fv1(∀(X,G,T),I,R) :- !,fv(T,Ts),gfv(G,Ts2), union_eq(Ts2,Ts,Ts3),
subtract_eq(Ts3,[X],R1), union_eq(I,R1,R).
gfv(Γ,Xs) :- foldr(gfv1, Γ, [], Xs).% 型環境置換
gfv1((_,T), Fv1,R) :- fv(T,T_),union_eq(Fv1,T_,R).%todo
cfv(C,R) :- maplist(cfv1,C,R1),foldr(union_eq,R1,[],R).
cfv1((_,G),R) :- gfv(G,R).
fvは自由型変数を取得します。fv1が１つ１つの要素の処理です。gfvが型環境の自由型変数を求め、cfvは制約の自由型変数を求めます。
cdom(C,R) :- maplist(cdom1,C,R). % ドメイン
cdom1((A,_),A).
creg(C,R) :- cdom(C,R1), foldr(creg1(C),R1,[],R). % リージョン(領域)
creg1(C,A,R1,R) :- capp(C,A,G), gfv(G,R2), union_eq(R1,R2,R).
capp(C,A,R) :- (A1,R) ∈ C,A1==A,!. % 適用
capp(_,_,[]).
これは論文にあった、制約のドメイン、制約のリージョン（領域）、制約の関数適用処理です。図には現れないので探すのが大変でした。
% 一般化 : 制約Cを一般化できたら環境から回収して清潔さを保つのがポイント
mem(F,A) :- call(F,As),!, A ∈ As. % 述語を実行してメンバ取り出し
memeq(F,A) :- call(F,As),!, member_eq(A,As). % 述語を実行してメンバ判定
tpgen(T,G,C,C_,R) :- mem(cdom(C),A), % CのドメインにあるAで
\+memeq(gfv(G),A), % 環境の自由変数になく
\+memeq(creg(C),A), % リージョン領域にもない
\+memeq(cdom(C_),A), % 元のドメインにもない
capp(C,A,Ca),!, % 制約をとりだし
%(memeq(gfv(Ca),A) ; memeq(fv(T),A)),!, % 追加条件
del_eq(C,A,C2),% 制約リストからAを除外
tpgen(∀(A, Ca, T), G, C2, C_,R).
tpgen(T,_,C,_,(T,C)).
mem,memeqは述語を実行してからメンバを取り出したり、メンバ判定をします。
tpgenが一般化の処理です。tpgenは型T,環境G、制約Cと元の制約Cを受取って、一般化された型Tと制約のペアを返します。
mem(cdom(C),A)でCのドメインにあるAの１つを取り出し、それ以降のmemeq述語の条件を満たしているAを検索し、capp述語で制約Caを取り出しています。関数型言語であれば、Cのドメインは１つの値ではなくリストデータでそこから条件に見合った値をとる処理を書くことになり単純にはかけないかも知れませんが、Prologでは順番に書くだけでうまく動作してくれます。
% 具体化
inst(T,C,(T,C)) :- var(T),!;T\= ∀(_,_,_),!. % ∀でなければそのまま
inst(∀(A,G,T),C,R) :- sub(A/B,T,T_),inst(T_,[(B,G)|C],R).% 新しいBで置換、制約追加
instはインスタンス化処理で、特に難しいことはありません。
% 単一化
mgu(_, T1,T2,C,C) :- T1==T2,!. % 同じ
mgu(G,A,T,C,R) :- var(A),!,mgu1(G,A,T,C,R).% 型変数なら単一化
mgu(G,T,A,C,R) :- var(A),!,mgu1(G,A,T,C,R).
mgu(G,K!T,K!T_,C,R) :- !,mgu(G,T,T_,C,R).% データ引数で単一化
mgu(G,(T1,T2),(T1_,T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%ペア
mgu(G,(T1->T2),(T1_->T2_),C,R) :- !,mgu(G,T1,T1_,C,R1),mgu(G,T2,T2_,R1,R).%関数
mgu(_,[],[],C,C) :- !.% ユニット
mgu(_,T1,T2,(_,_),_) :- failwith('mgu error ~w ~w', [T1,T2]).
mgu1(G,A,T,C,R) :- capp(C,A,G1), del_eq(C,A,C2),% 変数制約取得、制約の回収※1
A=T, mgn(G,(A,G1),C2,R),!.% 単一化、回収制約正規化
mgu1(_,A,T,_,_) :- failwith('mgu1 error ~w ~w',[A,T]).
% 正規化アルゴリズム
mgn(G,(A,G1),C,R) :- foldl(mgn1(G,A),G1,C,R). % 制約G1でループ
mgn1(G,A,(D,T),C,R) :- var(A),capp(C,A,G1),!,% 変数なら制約取得
((D_,T_)∈G1,D==D_,!,mgu(G,T,T_,C,R) % クラス有り、単一化
; R=[(A,[(D,T)|G1])|C]).% クラス無し、制約追加(※1戻す)
mgn1(G,K!KT,(D,T),C,R) :- !,(inst C_=>K_!KT_:D_!T_)∈G,K_==K,D_==D,% 実装検索
!,sub(KT_/KT,T_,T2_),mgu(G,T,T2_,C,C2),% クラス引数単一化
csub(KT_/KT,C_,C2_),% 制約を置換して実体化
foldr(mgn(G),C2_,C2,R).% 実体化した制約で正規化ループ
mgn1(G,(T1,T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% ペア
mgn1(G,(T1->T2),Y,C,R) :- mgn1(G,T1,Y,C,R1), mgn1(G,T2,Y,R1,R).% 関数
mgn1(_,[],_,C, C). % ユニット
mgn1(G,T1,Y,C,_) :- failwith('error:~w',[mgn1(G,T1,Y,C)]).
単一化処理はmguで行います。
mgu1は片方が型変数だった場合に呼び出され、変数制約を取得して制約を一度制約環境から取り除き、取り除いた制約はmgnで正規化します。
mgnはmgn1をループで呼び出すだけです。
mgn1は型のパターンによって正規化の処理を行います。
変数なら制約を朱トクして、クラスがある場合は単一化し、クラスがなければ制約を元に戻します。
型クラスなら、instの実装を検索し、クラス引数を単一化して制約を置換し実体化して、実体化した制約で正規化を行います。
ペアの場合は、両方の方についてmgn1を呼び出します。関数も同様に両方の型についてmgn1を呼び出します。ユニットなら何もしません。
% 型推論(式)
tp(I,_,C,(int,C)) :- integer(I),!.
tp(F,_,C,(float,C)) :- float(F),!.
tp([],_,C,([],C)). :- !. % unit
tp(λ(X,E),G,C,((A->T1),C1)) :- !,tp(E,[(X,A)|G],[(A,[])|C],(T1,C1)).
tp((let X=E1;E2),G,C,R) :- !,tp(E1,G,C,(T1,C1)),tpgen(T1,G,C1,C,(T,C2)),
tp(E2,[(X,T)|G],C2,R).
tp(X,G,C,R) :- atom(X),!,(X,T) ∈ G, inst(T,C,R).
tp((E1$E2),G,C,(A,C3)) :- !,tp(E1,G,C,(T1,C1)),!,tp(E2,G,C1,(T2,C2)),!,
mgu(G,T1,(T2->A),([(A,[])|C2]),C3),!.
tp は式の型推論の本体です。特に難しいことはしません。
% syntax suger
td(class A:D where X:T;P,G,C,R)
:- var(D),var(A),!,td(class A:D![]where X:T;P,G,C,R).
td(inst K!KT:D where X=E;P,G,C,R)
:- !,td(inst []=>K!KT:D where X=E;P,G,C,R).
td(inst C_=>K!KT:D where X=E;P,G,C,R)
:- var(D),!,td(inst C_=>K!KT:D![]where X=E;P,G,C,R).
% 型推論(宣言)
td(val X:T;P,G,C,R) :- !,td(P, [(X,T)|G], C,R).
td(type X=T;P,G,C,R) :- !,X=T,!,td(P, G, C,R).
td(class A:D!DT where X:T;P,G,C,R)
:- var(A),var(D),!, gfv([(D,DT)],YFV),!,
foldr(addall,YFV,∀(A,[(D,DT)],T), T2),!,
td(P, [(X,T2)|G], C, R).
td(inst C_=>K!KT:D!T where X=E;P,G,C,R)
:- var(D),!, G_=[inst C_=>K!KT:D!T|G],!,
tp(X, G_, C,(T1,C1)),!,tpgen(T1,G_,C1,C,(_,_)),!,
tp(E, G_, C,(T2,C2)),!,tpgen(T2,G_,C2,C,(T2_,_)),!,
getG(T2_,T2_C),!,
capp(C_,K!KT,CKT),!,maplist({CKT}/[A]>>member_eq(A,CKT),T2_C),!,
td(P,G_,C,R).
td(E,G,C,R) :- !,tp(E,G,C,R),!.
tdは宣言部分の型推論の本体です。内部でtpを呼び出したりします。
最初の３つの処理は構文糖の処理です。
val,typeも変数の型宣言と型宣言の処理でテストする際に便利なので追加した処理です。
一番最後のパターンは単なる式の処理です。
下から３番目のclassと２番目のinstの処理が重要な処理です。
classの処理では、D,DTから自由変数YFVを取り出し、型に加えて環境に追加して後続のプログラムを検査します。
instの処理は、インスタンスを環境に加え、その環境でのXとEを型推論し、一般化したあと、
制約環境を取りだし、制約環境を型コンストラクタに適用して型検査した後、後続のプログラムを検査します。
getG(∀(_,G,T),G2) :- getG(T,G1), union_eq(G,G1,G2).
getG(_,[]).
addall(A,T,∀(A,[],T)).
この２つはtdの補助述語です。
tp3(G, E, T3) :- tp(E,G,[],(T1,C1)), tpgen(T1,G,C1,[],(T3,_)).
tp1(E,T) :- tp3([],E,T).
tpp(P,T2):- td(P,[],[],(T,C)),tpgen(T,[],C,[],(T2,_)).
tp3,tp1,tppは型推論を使ってよりテストしやすくするための述語です。
既存研究
thih 1 の型クラスの実装は Haskell の型システムを再現する為、かなり大きいので理解しづらいものがありました。 ワドラーの論文 2 は、説明としては素晴らしいのですが、宣言的であるため実装できませんでした。 型クラスの実装の分かりやすい説明は、3 などにあるのでイメージはだいたいつかめるでしょう。型クラスの小さな実装は、２つの研究があります。１つ目は カン・チェン、ポール・フダク、マーティン・オデスキーの Parametric Type Classes 4 で、特徴はパラメータも持てる点です。 Nipkow らの Mini-Haskell の研究 5 はより小さく汎用的なものを目指したようです。ワドラーらの A second look at overloading 6 は型クラスの概念もなくシンプルで型クラスの実装の練習課題として適していると言えるでしょう。
貢献
Prolog の実装では subst を意識からなくすことでより短く本質を書くことが出来ました。実際に動作する宣言的で短いコードは（筆者の知るところでは）ありませんでした。
この実装は、複数の関数を持った型クラスの実装ではありませんが本質をよく捉えています。分かりやすいかどうかはわからないのですが、参考になれば幸いです。
参考文献
-
Typing Haskell in Haskell https://web.cecs.pdx.edu/~mpj/thih/thih.pdf ↩
-
How to make ad-hoc polymorphism less ad hoc https://pdfs.semanticscholar.org/cc7f/2242dba6f09023128897762d07517f13ba4a.pdf ↩
-
Type Class Implementation for Dummies https://github.com/camlspotter/ocaml-zippy-tutorial-in-japanese/blob/master/tclass.md ↩
-
Parametric Type Classes http://haskell.cs.yale.edu/wp-content/uploads/2011/03/ParametricTC-LFP92.pdf ↩
-
Nipkow の Mini-Haskell 研究 Type Checking Type Classes https://www.researchgate.net/profile/Christian_Prehofer/publication/220997948_Type_Checking_Type_Classes/links/0046353be9e60e89f7000000.pdf ↩
-
A second look at overloading これは、型クラスですらなくなっている。 ↩