オーバーロードの第2の見方 - A Second Look at Overloading 実装

ワドラー先生とオダスキー先生のA Second Look at OverloadingをPrologで実装してみたものです。

```prolog
:- expects_dialect(sicstus).
:- current_prolog_flag(argv, [M]),!,format('use ~w\n',[M]),use_module(M) ;
   use_module(over5).

:- begin_tests(main).

	test(mono) :- [] ⱶ (let f  = λ(x,x); f $ 1)           : int.
	test(poly) :- [] ⱶ (let id = λ(x,x); ((id $ id) $ 1)) : int.

	test(data) :- [] ⱶ (
			type Point = point![float,float];
			val point : (float→float→Point);
			val pt1 : (Point→float);
			val pt2 : (Point→float);
			val (+) : (float→float→float);
			let p = point $ 2.0 $ 3.0;
			(+) $ (pt1 $ p) $ (pt2 $ p)
		) : float.
	test(inst):- [] ⱶ (
			type Point = point![float,float];
			val point: (float→float→Point);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			let xx = λ(p, xcoord $ p);
			let p = point $ 2.0 $ 3.0;
			xx $ p
		): float.
	test(inst):-[] ⱶ (
			type Point = point![float,float];
			val point: (float→float→Point);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			let xx = λ(p, xcoord $ p);
			xx
		): ∀(A,[],∀(B,[xcoord:(B→A)],(B→A))).

	test(inst):-[] ⱶ (
			type Point = point![float,float];
			val point: (float→float→Point);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			let xx = λ(p, xcoord $ p);
			let xf = λ(xx, λ(p, xx $ p));
			xf
		): ∀(A,[],∀(B,[],((B→A)→B→A))).
		
	test(inst):-[] ⱶ (
			type Point = point![float,float];
			val point: (float→float→Point);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			let xx = λ(p, xcoord $ p);
			let xf = λ(xx, λ(p, xx $ p));
			xf $ xx
		): ∀(A,[],∀(B,[xcoord:(B→A)],(B→A))).

	test(inst):-[] ⱶ (
			type Point = point![float,float];
			val point: (float→float→Point);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			let xx = λ(p, xcoord $ p);
			let xf = λ(xx, λ(p, xx $ p));
			xf $ xx $ (point $ 1.0 $ 2.0)
		): float.

	test(inst):-[] ⱶ (
			type Point = point![float];
			val point: (float→float);
			val ptx: (Point→float);
			inst xcoord: (Point→float) = λ(u,ptx$u);
			λ(p,xcoord $ p)
		): ∀(A,[],∀(B,[xcoord:(B→A)],(B→A))).

	test(isfree):-[] ⱶ (
			type P = p![int];
			val ptx: (P→int);
			inst x: (P→int) = λ(u,ptx$u);
			λ(p,(let xx = x $ p; xx))
		): ∀(A,[],∀(B,[x:(B→A)],(B→A))).

	test(dict) :- [] ⱶ (
			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);
			inst xcoord : (Point→float) = λ(u, pt1 $ u);
			inst ycoord : (Point→float) = λ(u, pt2 $ u);
			inst xcoord : (CPoint→float) = λ(u, cpt1 $ u);
			inst ycoord : (CPoint→float) = λ(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.

:- end_tests(main).

:- run_tests.
:- halt.
```

この型検査を行うプログラムを以下に示します:

```prolog
:- module(_,[foldr/4,tv/2, ⱶ/2,gen/4,newinst/3,unify/3,ga/3]).
:- op(500,yfx,[!]).
:- op(600,yfx,[∈,$,\]).
:- op(600,xfy,[→]).
:- op(800,fy,[let,inst,type,val]).
:- op(900,xfx,[ⱶ]).
:- set_prolog_flag(occurs_check, true).

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_),!.
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,!,halt. % エラー処理
cp(A/B,X,B) :- X==A. % Xが変数AならBに置き換え
cp(AB,X,R) :- compound(X), X=..Xs,!,maplist(cp(AB),Xs,R_),R=..R_,!.
cp(_,I,I) :- !.
% -------------------------------------------------

tv(X,R) :- walk(tv1,X,[],R),!. % 自由型変数取得
tv1(X,I,R) :- var(X), union_eq(I,[X],R).
tv1(∀(X,Πa,T),I,R):-walk(tv1,[T,Πa],I,R_),subtract_eq(R_,[X],R).

ga(C, A, Ga) :- foldr(ga1(A),C,[],Ga).      % 制約集合からAの制約取得
ga1(A, O:A_→T, C, [O:A_→T|C]) :- A == A_. % 変数の実態でパターンマッチ
ga1(_,_,C,C).

% 一般化 [Let],[Inst]で使用
gen(T,Γ,C,T_) :- free(T,A),           % T内で自由な変数Aで一般化したい
                 ga(C,A,Γa),          % Aの制約Γa
                 subtract_eq(Γ,Γa,Γ_),% Γから制約Γaを引いたΓ_
                 \+free(Γ_,A),        % Γ_でAが自由なら一般化不能
                 !,gen(∀(A,Γa,T),Γ_,C,T_).% Γ_の環境で再度一般化
gen(T,_,_,T).
gen(T,Γ,C,(T_,C)) :- gen(T,Γ,C,T_).
free(Γ,A) :- tv(Γ,ΓTv),member(A,ΓTv).      % 環境 Γ で A が自由か

% 具体化 [VarU],[VarO]で使用
newinst(T,C,(T,C))            :- var(T),!.
newinst(∀(A,Πa,T),C,(T2,C2)) :- !,cp(A/_,Πa/T,Πa_/T_), % Aを_に変える
                                 union_eq(Πa_,C,C_), % 制約を環境に保存
                                 newinst(T_, C_, (T2,C2)).
newinst(T,C, (T,C)).

% 単一化 [App]で使用
unify(_, T1,T2)        :- T1==T2,!. % 同じ
unify(C, T,A)          :- var(A),T=A, watch(C, A),!. % 片方が型変数
unify(C, A,T)          :- var(A),T=A, watch(C, A),!. % 単一化を捕捉
unify(C, T1→T2,T3→T4):- unify(C,(→)![T1,T2],(→)![T3,T4]),!. % 関数
unify(C, D!Ts1,D!Ts2)  :- maplist(unify(C),Ts1,Ts2). % データコンストラクタ
unify(C, T1,T2)        :- failwith('error ~w',[unify(C,T1,T2)]).
watch(C, A)       :- ga(C,A,Γa), maplist(mkinst(C),Γa). % Aの制約でループ
mkinst(C, O:A→T) :- (O:B→T_)∈C,A==B,unify(C,T,T_). % 制約の型を単一化

% 型付け規則
Γ ⱶ P : T                   :- op(Γ, P : T).
op(Γ,P : T)                 :- o(Γ, [], P : T1,C1),!, gen(T1,[],C1,T).
o(_,C,I:int,C)              :- integer(I).
o(_,C,F:float,C)            :- float(F).
o(Γ,C,λ(U, E):A→T1,C1)     :- o([U:A|Γ],C, E:T1,C1).
o(Γ,C,(let U=E;E_):T2,C2)   :- o(Γ,C, E:T0,C0), gen(T0,Γ,C0,T1),
                               o([U:T1|Γ],C0, E_:T2,C2).
o(Γ,C,U:T_,C_)              :- atom(U), (U:T)∈Γ,!, newinst(T,C,(T_,C_)),!.
o(Γ,C,(inst O:ΣT=E;P):T,C_) :- o(Γ,[O:ΣT|C], E:T0,C0),gen(T0,Γ,C0,_),
                               o(Γ,C0, P:T,C_).
o(_,C,O:T_,C_)              :- atom(O),(O:_)∈C,!,
                               newinst(∀(B,[],∀(A,[O:A→B],A→B)),C,(T_,C_)).
o(_,_,X:_,_)                :- atom(X), failwith('unbound variable ~w',[X]).
o(Γ,C,(E $ E_):A,C2)        :- !,o(Γ,C, E:T1,C1),!,o(Γ,C1, E_:T2,C2),
                               !,unify(C2, T1, T2→A),!.
o(Γ,C,(type X=T1;P):T,C_)   :- X = T1, o(Γ,C,P:T,C_),!.
o(Γ,C,(val X:T1;P):T,C_)    :- o([X:T1|Γ],C,P:T,C_),!.
```