ワドラー先生とオダスキー先生のA Second Look at Overloadingを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.
この型検査を行うプログラムを以下に示します:
:- 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_),!.