この記事は言語実装 Advent Calendar 2020の16日目の記事です。
Prologに慣れていない人のためにPrologでの単相の型システムを示し、線形型システムであるSystem-Fo(Fポップ)およびアフィン型システムSystem-Fa(Fアフィン)を実装例を示します。
アフィン型システムというとRustのオーナーシップの型システムが近いのですが、Rustのような型システムの本質的部分を取り出して実装したものがアフィン型システムです。難解な型システムの数式は嫌がらせのように感じるかもしれませんが、Prologを使えば実際に動かせるのでより理解しやすいものになっているはずです。
1. 単相型システムとlet多相型システム
まずは、Prologで単純な型推論を作ってみます:
% simple.pl
:- op(500,yfx,$),op(600,xfy,:),op(600,xfy,[→]).
t(_,I,int):- integer(I),!. % T-Int
t(_,true,bool). % T-True
t(_,false,bool). % T-False
t(Γ,if(E1,E2,E3),T):- t(Γ,E1,bool),t(Γ,E2,T),t(Γ,E3,T). % T-If
t(Γ,E1<E2,bool):- t(Γ,E1,int),t(Γ,E2,int). % T-Lt
t(Γ,E1+E2,int):- t(Γ,E1,int),t(Γ,E2,int). % T-Add
t(Γ,X,T):- member(X:T,Γ),!. % T-Var
t(Γ,λ(X,E),T1->T):- t([X:T1|Γ],E,T). % T-Lam
t(Γ,E1$E2,T):- t(Γ,E1,T1->T),t(Γ,E2,T1). % T-App
:- begin_tests(t).
test(tint):- t([],10,int).
test(ttrue):- t([],true,bool).
test(tfalse):- t([],false,bool).
test(tif):- t([],if(if(true,true,false),1,2),int).
test(tlt):- t([],1<2,bool).
test(tadd):- t([],1+2+3,int).
test(tvar):- t([x:int],x,int).
test(tlam):- t([],λ(y,λ(x,x+y)),int->int->int).
test(tapp):- t([],λ(y,λ(x,x+y))$1$1+2,int).
:- end_tests(t).
:- run_tests.
:- halt.
Prologは一階述語論理を自動証明するシステムなので単相の型システムは型付け規則をただ書くだけで実装できてしまいます。
SWI-Prologのテストはbegin_tests/1とend_tests/1の間のtest/1述語として記述してrun_tests/1で実行します。
$ swipl simple.pl
と実行することでテストを実行できます。
SWI-Prologのインストールは brew install swi-prolog あるいは apt install swi-prolog などで出来ます。
let多相な型推論は以下のように書けます:
:- op(600,xfy,$).
copy(T,T1):- assert(c(T)),retract(c(T1)).
inst(mono(T),T).
inst(poly(G,T1),T):-copy(G/T1,G/T).
e(_,I,int):- integer(I),!.
e(_,true,bool):-!.
e(_,false,bool):-!.
e(Γ,E1+E2,int):-e(Γ,E1,int),e(Γ,E2,int).
e(Γ,if(E1,E2,E3),T):- e(Γ,E1,bool),e(Γ,E2,T),e(Γ,E3,T).
e(Γ,X,T):- member(X:SC,Γ),!,inst(SC,T).
e(Γ,λ(X,E),T->T1):- e([X:mono(T)|Γ],E,T1).
e(Γ,E1$E2,T):- e(Γ,E1,T2->T),e(Γ,E2,T2).
e(Γ,let(X=E,E2),T):- e(Γ,E,T1),e([X:poly(Γ,T1)|Γ],E2,T).
:- e([],let(f=λ(x,x),f$((f$λ(t,t+1))$1)),T),writeln(T).
:- halt.
2. 軽量な線形型システム
さて、次は、線形型システムを作ってきましょう。
線形型は線形論理を型に応用したものです。
線形論理は、縮約 contraction (資源を複製する能力)と弱化 weakning(資源を捨てる能力)の性質を制限することによって資源の使用をモデル化します。
今回は PPL19 の論文 Lightweight Linear Types in System F◦,Karl Mazurak,Jianzhou Zhao,Steve Zdancewic を元に軽量な線形型システムをPrologで実装しました:
% systemfo.pl
:- op(500,yfx,$),op(600,xfy,:),op(600,xfy,[→,in]),op(600,fy,[ʌ,λ]).
% 置換
s(X,Y,X,Y) :- !.
s(_,_,X,X) :- atom(X),!.
s(A,Y,T-K→T1,T_-K→T1_) :- !,s(A,Y,T,T_),s(A,Y,T1,T1_).
s(A,_,∀(A:K,T),∀(A:K,T)) :- !.
s(A,Y,∀(X:K,T),∀(X:K,T_)) :- s(A,Y,T,T_).
% カインド
k(Γ,T:K) :- member(T:K,Γ),!. % K-TVar
k(Γ,∀(A:K,T):K_) :- k([A:K|Γ],T:K_). % K-All
k(Γ,(T-K→T1):K) :- k(Γ,T:_),k(Γ,T1:_). % K-Arr
% 型付け規則
t(Γ;[],X:T,[]) :- atom(x),member(X:T,Γ),!. % T-UVar
t(_;Δ,X:T,Δ1) :- atom(x),select(X:T,Δ,Δ1),!. % T-LVar
t(Γ;Δ,(ʌ T:K→V): ∀(T:K,T1),[]) :- \+k(Γ,T:_),t([T:K|Γ];Δ,V:T1,[]). % T-TLam
t(Γ;Δ,(λ X:T-K→E):(T-K→T1),[]) :- \+member(X:_,Δ),\+member(X:_,Γ), % T-Lam
k(Γ,T:o),t(Γ;[X:T|Δ],E:T1,[]). % B-Lin
t(Γ;[],(λ X:T-K→E):(T-K→T1),[]):- \+member(X:_,Γ), % T-Lam
k(Γ,T:x),t([X:T|Γ];[],E:T1,[]). % B-Un
t(Γ;Δ,E$[T]:T2,[]) :- k(Γ,T:K),t(Γ;Δ,E: ∀(A:K,T1),[]),
s(A,T,T1,T2). % T-TApp
t(Γ;Δ,E$E1:T,[]) :- t(Γ;Δ,E1:T1,Δ1),
t(Γ;Δ1,E:(T1-_→T),[]). % T-App
t(Γ;Δ,(let(X=E)in E2):T,Δ2) :- t(Γ;Δ,E:T1,Δ1),
t([X:T1|Γ];Δ1,E2:T,Δ2). % T-Let
t(Γ;Δ,(E;E2):T,Δ2) :- t(Γ;Δ,E:unit,Δ1),t(Γ;Δ1,E2:T,Δ2). % T-Semi
t(Γ,(ΛX:K→V):T,Δ) :- atom_concat(ʌ,X,ΛX),t(Γ,(ʌ X:K→V):T,Δ).
t(Γ,(ΛX:K→V):T,Δ) :- atom_concat(λ,X,ΛX),t(Γ,(λ X:K→V):T,Δ).
t(E,T) :- t([];[],E:T,_),!.
t(E) :- \+t([];[],E:_,_).
:- begin_tests(t).
test(simple) :- t(ʌa:x→λy:a-x→y,∀(a:x,a-x→a)).
test(linearSimple) :- t(ʌa:o→λz:a-x→z,∀(a:o,a-x→a)).
test(tapp) :- t(ʌt:x→λy:t-x→(ʌa:x→λz:a-x→z)$[t]
,∀(t:x,t-x→t-x→t)).
test(type) :- t(ʌt:x→λy:t-x→λz: ∀(a:x,a-x→a)-x→z$[t]$y
,∀(t:x,t-x→ ∀(a:x,a-x→a)-x→t)).
test(unrestricted) :- t(ʌa:x→λw:a-o→(λy:a-o→λz:a-o→y)$w$w
,∀(a:x,a-o→a)).
test(curry) :- t(ʌa:x→ʌb:x→ʌc:x→λw:a-o→λy:b-o→λz:c-o→z
,∀(a:x,∀(b:x,∀(c:x,a-o→b-o→c-o→c)))).
test(badArgument) :- t(ʌa:x→ʌb:x→λw:a-o→(λy:b-o→y)$w). % (λy:b-o→y) : b -o-> b なのに w:a を引数として呼び出し
test(callNonFunction):- t(ʌa:x→ʌb:x→λw:a-o→w$(λy:b-o→y)). % 関数ではないものを呼び出し
test(curryUnused) :- t(ʌa:x→ʌb:o→ʌc:o→λx:a-o→λy:b-o→λz:c-o→z).
test(dupulicate) :- t(ʌa:x→ʌb:o→λw:a-o→λw:b-o→w).
test(linearMixed) :- t(ʌa:o→λw:a-o→λy:a-x→y).
test(linearOrdered) :- t(ʌa:x→ʌb:o→λw:a-o→λy:b-o→w).
test(linearTwice) :- t(ʌa:x→ʌb:o→λw:b-o→(λy:b-o→λz:a-o→y)$w$w).
test(linearUnused) :- t(ʌa:o→λv:a-o→λw:a-o→(λy:a-o→λz:a-o→y)$v$w).
test(files) :- t(ʌfp:o→
ʌchar:x→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λclose:(fp-x→unit)-x→
close $ (open $ fname),
∀(fp:o,∀(char:x,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→unit)-x→unit))))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λdata:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λwrite:(fp-x→string-x→fp)-x→
λclose:(fp-x→unit)-x→
close $ (read $ (read $ (write $ (open $ fname) $ data))),
∀(fp:o,∀(string:x,∀(unit:x,
string-x→
string-x→
(string-x→fp)-x→
(fp-x→fp)-x→
(fp-x→string-x→fp)-x→
(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→close1 $ (open $ fname)) $ (λf:fp-x→close $ (read $ f))
,
∀(fp:o,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→fp)-x→(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→
(λread1:(fp-x→fp)-x→
close1 $ (read1 $ (open $ fname))
)
) $ (λf:fp-x→close $ (read $ f)) $ (λf:fp-x→read $ f)
,
∀(fp:o,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→fp)-x→(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λu:unit-x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→
(λread1:(unit-x→fp-x→fp)-x→
close1 $ ((read1 $ u)$ (open $ fname))
)
) $ (λf:fp-x→close $ (read $ f)) $ (λf:unit-x→read)
,_).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λu:unit-x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
let(close1=λf:fp-x→close $ (read $ f)) in
let(read1=λu1:unit-x→λf:fp-x→read$f) in
let(f=open $ fname) in
let(f=read1 $ u $ f) in
close1 $ f
,_).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λread:(fp-x→fp)-x→
(λread1:(fp-x→unit-x→fp)-x→
(read1 $ (open $ u) $ u)
) $ (λf1:fp-x→λu:unit-x→read$f1)).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
let(u1= close $ f1) in
close $ f2,
T),writeln(T).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(fn= (λu1:unit-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
let(u1= close $ f1) in
close $ f2
)) in
fn $ u
,
T),writeln(T).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(fn= (λu1:unit-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
(close $ f1; close $ f2)
)) in
fn $ u
,
T),writeln(T).
:- end_tests(t).
:- run_tests.
:- halt.
実行方法は
$ swipl systemfo.pl
System-System F◦(「Fポップ」と発音) は非常に小さいながらも線形型を実現しています。
Fポップという名前は線形論理型言語ロリポップのポップから命名したものでしょう。-o 演算子がアメに似ているのが由来だと思います。
線形型システムの実装方法は様々あるわけですが、System-Foはカインドベースに型システムを構築することで小さく作れたそうです。
Prologの実装はいくつか作ってみたのですが矢印の使い方を工夫して見た目を整えました。
3. 軽量なアフィン型システム
さて、線形型が実装できたのであれば部分構造論理型の仲間であるアフィン型のようなものも作れるはずです。
線形論理は縮約と弱化の能力を捨てた論理でしたがアフィン論理は縮約のみを捨てた論理なので、線形論理の弱化の性質を生かすことで得られます。
線形型はリソースの削除を自動的にしてくれないので自前で削除しなければなりませんが、アフィン型は自前削除しなくても自動的に削除してくれるように変更すればよいだけです。
ということで実装してみました:
% systemfa.pl
:- op(500,yfx,$),op(600,xfy,:),op(600,xfy,[→,in]),op(600,fy,[ʌ,λ]).
% 置換
s(X,Y,X,Y) :- !.
s(_,_,X,X) :- atom(X),!.
s(A,Y,T-K→T1,T_-K→T1_) :- !,s(A,Y,T,T_),s(A,Y,T1,T1_).
s(A,_,∀(A:K,T),∀(A:K,T)) :- !.
s(A,Y,∀(X:K,T),∀(X:K,T_)) :- s(A,Y,T,T_).
% カインド
k(Γ,T:K) :- member(T:K,Γ),!. % K-TVar
k(Γ,∀(A:K,T):K_) :- k([A:K|Γ],T:K_). % K-All
k(Γ,(T-K→T1):K) :- k(Γ,T:_),k(Γ,T1:_). % K-Arr
% 型付け、変換規則
t(Γ;[],X:T,X,[]) :- atom(x),member(X:T,Γ),!. % T-UVar
t(_;Δ,X:T,X,Δ1) :- atom(x),select(X:T,Δ,Δ1),!. % T-LVar
t(Γ;Δ,(ʌ T:K→V): ∀(T:K,T1),(ʌ T:K→V_),[])
:- \+k(Γ,T:_),t([T:K|Γ];Δ,V:T1,V_,_). % T-TLam
t(Γ;Δ,(λ X:T-K→E):(T-K→T1),(λ X:T-K→E_),Δ2)
:- \+member(X:_,Δ),\+member(X:_,Γ), % T-Lam
k(Γ,T:o),t(Γ;[X:T|Δ],E:T1,E_1,Δ1),% B-Lin
( select(X:T,Δ1,Δ2)-> E_=(delete$X;E_1)
; Δ2=Δ1,E_=E_1).
t(Γ;[],(λ X:T-K→E):(T-K→T1),(λ X:T-K→E_),[]):- \+member(X:_,Γ), % T-Lam
k(Γ,T:x),t([X:T|Γ];[],E:T1,E_,[]).% B-Un
t(Γ;Δ,E$[T]:T2,E_$[T],[]) :- k(Γ,T:K),t(Γ;Δ,E: ∀(A:K,T1),E_,[]),
s(A,T,T1,T2). % T-TApp
t(Γ;Δ,E$E1:T,E_$E1_,[]) :- t(Γ;Δ,E1:T1,E1_,Δ1),
t(Γ;Δ1,E:(T1-_→T),E_,[]). % T-App
t(Γ;Δ,(let(X=E)in E2):T,(let(X=E_)in E2_),Δ2)
:- t(Γ;Δ,E:T1,E_,Δ1),
t([X:T1|Γ];Δ1,E2:T,E2_,Δ2). % T-Let
t(Γ;Δ,(E;E2):T,(E_;E2_),Δ2) :- t(Γ;Δ,E:unit,E_,Δ1),
t(Γ;Δ1,E2:T,E2_,Δ2). % T-Semi
t(Γ,(ΛX:K→V):T,(ΛX:K→V_),Δ) :- atom_concat(ʌ,X,ΛX),
t(Γ,(ʌ X:K→V):T,(ʌ X:K→V_),Δ).
t(Γ,(ΛX:K→V):T,(ΛX:K→V_),Δ) :- atom_concat(λ,X,ΛX),
t(Γ,(λ X:K→V):T,(λ X:K→V_),Δ).
t(E,T) :- t([];[],E:T,E,[]),!.
t(E,E_,T) :- t([];[],E:T,E_,[]),!.
t(E) :- \+t([];[],E:_,_,[]).
:- begin_tests(t).
test(simple) :- t(ʌa:x→λy:a-x→y,∀(a:x,a-x→a)).
test(linearSimple) :- t(ʌa:o→λz:a-x→z,∀(a:o,a-x→a)).
test(tapp) :- t(ʌt:x→λy:t-x→(ʌa:x→λz:a-x→z)$[t]
,∀(t:x,t-x→t-x→t)).
test(type) :- t(ʌt:x→λy:t-x→λz: ∀(a:x,a-x→a)-x→z$[t]$y
,∀(t:x,t-x→ ∀(a:x,a-x→a)-x→t)).
test(unrestricted) :- t(ʌa:x→λw:a-o→(λy:a-o→λz:a-o→y)$w$w
,∀(a:x,a-o→a)).
test(curry) :- t(ʌa:x→ʌb:x→ʌc:x→λw:a-o→λy:b-o→λz:c-o→z
,∀(a:x,∀(b:x,∀(c:x,a-o→b-o→c-o→c)))).
test(badArgument) :- t(ʌa:x→ʌb:x→λw:a-o→(λy:b-o→y)$w). % (λy:b-o→y) : b -o-> b なのに w:a を引数として呼び出し
test(callNonFunction):- t(ʌa:x→ʌb:x→λw:a-o→w$(λy:b-o→y)). % 関数ではないものを呼び出し
test(dupulicate) :- t(ʌa:x→ʌb:o→λw:a-o→λw:b-o→w).
test(linearOrdered) :- t(ʌa:x→ʌb:o→λw:a-o→λy:b-o→w).
test(linearTwice) :- t(ʌa:x→ʌb:o→λw:b-o→(λy:b-o→λz:a-o→y)$w$w).
test(curryUnused) :- t(ʌa:x→ʌb:o→ʌc:o→λx:a-o→λy:b-o→λz:c-o→z,
ʌa:x→ʌb:o→ʌc:o→λx:a-o→λy:b-o→(delete$y;λz:c-o→z),
∀(a:x,∀(b:o,∀(c:o,a-o→b-o→c-o→c)))).
test(linearMixed) :- t(ʌa:o→λw:a-o→λy:a-x→y,
ʌa:o→λw:a-o→(delete$w;λy:a-x→y),
∀(a:o,a-o→a-x→a)).
test(linearUnused) :- t(ʌa:o→λv:a-o→λw:a-o→(λy:a-o→λz:a-o→y)$v$w,
ʌa:o→λv:a-o→λw:a-o→(λy:a-o→λz:a-o→(delete$z;y))$v$w,
∀(a:o,a-o→a-o→a)).
test(files) :- t(ʌfp:o→
ʌchar:x→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λclose:(fp-x→unit)-x→
close $ (open $ fname),
∀(fp:o,∀(char:x,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→unit)-x→unit))))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λdata:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λwrite:(fp-x→string-x→fp)-x→
λclose:(fp-x→unit)-x→
close $ (read $ (read $ (write $ (open $ fname) $ data))),
∀(fp:o,∀(string:x,∀(unit:x,
string-x→
string-x→
(string-x→fp)-x→
(fp-x→fp)-x→
(fp-x→string-x→fp)-x→
(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→close1 $ (open $ fname)) $ (λf:fp-x→close $ (read $ f))
,
∀(fp:o,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→fp)-x→(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→
(λread1:(fp-x→fp)-x→
close1 $ (read1 $ (open $ fname))
)
) $ (λf:fp-x→close $ (read $ f)) $ (λf:fp-x→read $ f)
,
∀(fp:o,∀(string:x,∀(unit:x,string-x→(string-x→fp)-x→(fp-x→fp)-x→(fp-x→unit)-x→unit)))
).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λu:unit-x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
(λclose1:(fp-x→unit)-x→
(λread1:(unit-x→fp-x→fp)-x→
close1 $ ((read1 $ u)$ (open $ fname))
)
) $ (λf:fp-x→close $ (read $ f)) $ (λf:unit-x→read)
,_).
test(files) :- t(ʌfp:o→
ʌstring:x→
ʌunit:x→
λu:unit-x→
λfname:string-x→
λopen:(string-x→fp)-x→
λread:(fp-x→fp)-x→
λclose:(fp-x→unit)-x→
let(close1=λf:fp-x→close $ (read $ f)) in
let(read1=λu1:unit-x→λf:fp-x→read$f) in
let(f=open $ fname) in
let(f=read1 $ u $ f) in
close1 $ f
,_).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λread:(fp-x→fp)-x→
(λread1:(fp-x→unit-x→fp)-x→
(read1 $ (open $ u) $ u)
) $ (λf1:fp-x→λu:unit-x→read$f1)).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
let(u1= close $ f1) in
close $ f2,
T),writeln(T).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(fn= (λu1:unit-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
let(u1= close $ f1) in
close $ f2
)) in
fn $ u
,
T),writeln(T).
test(files) :- t(ʌfp:o→
ʌunit:x→
λu:unit-x→
λopen:(unit-x→fp)-x→
λclose:(fp-x→unit)-x→
let(fn= (λu1:unit-x→
let(f1= (open $ u)) in
let(f2= (open $ u)) in
(close $ f1; close $ f2)
)) in
fn $ u
,
T),writeln(T).
:- end_tests(t).
:- run_tests.
:- halt.
テスト方法は:
$ swipl systemfa.pl
アフィン型システムではリソースが自動的に解放されるようになりました。
このように Prolog を使うと簡潔に線形型およびアフィン型を実装できます。
しかしながら、テストだけでは Prolog の実装が本当に正しいのかどうかわかりません。
この先の証明は Coq や Idris のような定理証明支援系の力が必要になります。
証明する事が亡くなって手持ち無沙汰になっている人がいらっしゃいましたら、各種証明に挑戦してみてはいかがでしょうか？