# Type Checking Type Classes

これは Tobias Nipkow と Christian Prehofer による型クラスの型検査の論文の実装です。

```:- tpp([(Colour, 'Colour'![]),
(Point, 'Point'![]),
(CPoint, 'CPoint'![])],
[('MkColour', (int->int->int->Colour)),
(c1, (Colour->int)),
(c2, (Colour->int)),
(c3, (Colour->int)),
(mkPoint, (float->float->Point)),
(pt1, (Point->float)),
(pt2, (Point->float)),
('MkCPoint', (float->float->Colour->CPoint)),
(cpt1, (CPoint->float)),
(cpt2, (CPoint->float)),
(cpt3, (CPoint->Colour)),
(sqr, (float->float)),
(sqrt, (float->float))],
class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
class('Ycoord',ycoord,∀(B,['Ycoord'],(B->float)));
inst('Point',[],'Xcoord', xcoord, λ(u,pt1\$u));
inst('Point',[],'Ycoord', ycoord, λ(u,pt2\$u));
inst('CPoint',[],'Xcoord', xcoord, λ(u,cpt1\$u));
inst('CPoint',[],'Ycoord', 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))
,float).
```

このような型クラスの型検査を以下に示します:

```:- module(np93b,
[foldr/4,fv/2,sub/3,gen/4,log/3,output/0,kcdom/3,tp3/4,tpp/4,tp1/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]).
term_expansion((A--B), (B:-A)).

lv(0). lv(1). lv(app). lv(inst).
log(Lv,X,P) :- lv(Lv), format(atom(V),X,P), bb_update(logs,Logs,[V|Logs]); true.
log(Lv,X) :- atom(X),log(Lv,X,[]).
log(Lv,X) :- format(atom(V),"~w",[X]),!,log(Lv,V,[]).
reset :- bb_put(logs,[]),!.
output() :- bb_get(logs,Logs),reverse(Logs,L),maplist(writeln,L).
failwith(A,Xs) :- format(A,Xs),nl,!,fail. % エラー処理
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).
foldr(_,[],S,S) :- !. % 畳み込み
foldr(F,[X|Xs],S,S_) :- foldr(F,Xs,S,S1),!,call(F,X,S1,S_),!.
zip([], [], []). % ２つのリストを１つにする
zip([X|Xs], [Y|Ys], [(X,Y)|Zs]) :- zip(Xs,Ys,Zs).
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す

fv(X      ,[X]) :- var(X), !.
fv(∀(X,_,T),R) :- !,fv(T,Ts), subtract_eq(Ts,[X],R).
fv(X,R) :- compound(X),X=..[_|Xs],!,maplist(fv,Xs,Ts_),foldr(union_eq,Ts_,[],R),!.
fv(_       ,[]) :- !.

sub(St,X,R) :- var(X),(X1,T)∈St,X==X1,!,sub(St,T,R).
sub(St,X,R) :- compound(X),X=..Xs,!,maplist(sub(St),Xs,R_),R=..R_,!.
sub(_,T,T).

gapp(G,T,S) :- (T1,S)∈G,T==T1.
gapp(_,_,[]).
gunion(G1,G2,G3) :- gdom(G1,Dom1),gdom(G2,Dom2),union_eq(Dom1,Dom2,Dom),
maplist(gunion1(G1,G2),Dom,G3),!.
gunion1(G1,G2,A,(A,G)) :- gapp(G1,A,G1_),gapp(G2,A,G2_),union_eq(G1_,G2_,G).
gdom(G,Ts) :- maplist(gdom1,G,Ts).
gdom1((T,_),T).
gsubtract(G,As,G_) :- foldr(gsubtract1(As),[],G,G_).
gsubtract1(As,(T,_),G,G) :- T_ ∈ As, T_==T.
gsubtract1(_,(T,C),G,[(T,C)|G]).

gen(G,Env,T1,(G_,T_)) :- fv(T1,Fv1),efv(Env,EFv),
subtract_eq(Fv1, EFv, Ans),
gsubtract(G,Ans,G_),
foldr(gen1(G),Ans,T1,T_).
gen1(G,A,T,∀(A,R,T)) :- gapp(G,A,R).
efv(Env,Fv) :- foldr(efv1,Env,[],Fv).
efv1((_,T), Fv,Fv_) :- fv(T,FvT),union_eq(Fv, FvT, Fv_).
esub(St,Env,Env_):- maplist(esub1(St),Env,Env_).
esub1(St,(X,T),(X,T_)) :- sub(St,T,T_).

inst(T,G,(T,G))        :- var(T), !.
inst(∀(An,Sn,T),G,TG) :- !, sub([(An,Bn)],T,T1),
gunion(G,[(Bn,Sn)],G1),
inst(T1,G1,TG).
inst(T,G,(T,G))        :- !.

mgu(T1,T2,[]) :- T1==T2,!.
mgu(A,T,[(A,T)]) :- var(A),!.
mgu(T,A,[(A,T)]) :- var(A),!.
mgu(T1,T2,R) :- T1=..[X1|Ts1],T2=..[X2|Ts2],X1==X2,!,
zip(Ts1,Ts2,Ts),foldl(mgu1,Ts,[],R).
mgu(T1,T2,_) :- failwith('mgu error ~w ~w',[T1,T2]).
mgu1((T1,T2),St,R):- sub(St,T1,T1_),sub(St,T2,T2_),
mgu(T1_,T2_,St_),union_eq(St, St_,R),!.

stdom(St,As) :- foldr(stdom1(St),St,[],As).
stdom1(St,(A,_),As,As) :- sub(St,A,A1), A==A1.
stdom1(_,(A,_),As,[A|As]).
unify(G,D,T1,T2,G_) :- mgu(T1,T2,St), !,stdom(St,As),!, %mguした置換ドメインで単一化ハンドリング
foldr(unify1(St,D),As,G,G_),% ドメインでループ
T1=T2. % 単一化
unify1(St,D,A,G,G_):- gapp(G,A,Ga), % 単一化された型変数の制約を取り出し
sub(St,A,A_), % 置換
gsubtract(G,[A],G1), % 消す
constrain(D,(A_,Ga),G1,G_). % 制約追加
constrain(_,(A,S),G,G_) :- var(A),!,gunion([(A,S)],G,G_). % 型変数なら 制約を伝搬
constrain(D,(K!Ts,S),G,G_) :- foldr(constr(D,K!Ts),S,G,G_). % 型コンストラクタをソートでループ
constrain(_,(_,_),G,G).
constr(D,K!Ts,C,G,G_) :- % 型コンストラクタの引数Tsに型クラスCを伝搬
inst(K,Ss,C) ∈ D,!, % 型クラスCのソートリスト取り出し
zip(Ts,Ss,TSs), foldr(constrain(D),TSs,G,G_). % 引数でループ
kcdom((K,C),D,Ss) :- inst(K,Ss,C) ∈ D,!. % インスタンス宣言時のソートリストがドメイン

i(λ(X,E),G,D,Env,((A->T),G_))
:- i(E,G,D,[(X,A)|Env],(T,G_)).
i(let X=E1;E2,G,D,Env,R):- !,i(E1,G,D,Env,(T1,G1)),
gen(G1,Env,T1,(G_,T_)),!,
i(E2,G_,D,[(X,T_)|Env],R),!.
i(X,G,_,Env,(T_,G_))    :- atom(X),!,(X1,T)∈Env,X1==X,inst(T,G,(T_,G_)),!.
i(E1\$E2,G,D,Env,(A,G_)) :- !,i(E1,G,D,Env,(T1,G1)),
i(E2,G1,D,Env,(T2,G2)),
unify(G2,D,T1, (T2->A),G_),!.
i(I,G,_,_,(int,G))    :- integer(I),!.
i(F,G,_,_,(float,G))  :- float(F),!.

ip(class(C,X,∀(A,[C|Cs],Q));P,G,D,Env,R) :-
ip(P,G,D,[(X,∀(A,[C|Cs],Q))|Env],R).
ip(inst(K,SS,C,X,E);P,G,D,Env,(Q_,G1)) :-
(X,T) ∈ Env, % 環境から関数の型取得
T = ∀(A,_,_), % 型を置換してパラメータ取り出し
D2=[inst(K,SS,C)| D], % インスタンス情報保存
ip(P,G,D2,Env,(Q_,G1)), % 後続プログラムの推論
% メソッドの検証
maplist(ip_mkvars,SS,Ag,As), % ソート推論用データ作成
gunion(G, Ag, Ag_), % Gにソート追加
i(E,Ag_,D2,Env,(Q2,_)), % 式の推論
sub([(A,K!As)], Q2, Q3), % 比較用に置換
mgu(Q3,Q2,_),!.
ip(E,G,D,Env,R) :- i(E,G,D,Env,R).
ip_mkvars(S,(X,S),X).

tp(I,St, Env, E, T_) :- reset,
log(1,'test ~i\n',[E]),
maplist(tpuni,St),!,
( call(I,E,[],[],Env,(T1,G1)),
log(1,'t1=~w\n', [T1]),
gen(G1, Env, T1,(_,T_)),!
; T_=error,!
; writeln(error),output,!,T_=error,!).
tpuni((A,A)).

tp3(St,Env,E,T_):-tp(i,St,Env,E,T_).
tpp(St,Env,E,T_):-tp(ip,St,Env,E,T_).
tp1(E,R) :- tp3([],[], E,R).
```

コード量は140行ほどです。
ソートを使ったほうが単純だというのがnipkowの主張です。