NP93

書きかけ

Nipkow の Mini-Haskell 研究

３つほど論文があります。NP95が最終的な結論のようです。

[NS91] 最初の論文。公開されていない。

[NP93] type_checking_type_class.pdf NS91を拡張しサブクラス的なことが可能

[NP95] type_reconstruction_for_type_classes.pdf NS93を拡張しサブクラスに対応

NS91でソートを導入した型システムを構築した。
NP93ではサブタイピングを制限としてできるようにしたけどサブタイプがなかった。
NP95ではサブタイピングを含めたほうが簡単なはずということで含めた。

np93b.pl

:- 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).
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_),!.
zip([], [], []). % ２つのリストを１つにする
zip([X|Xs], [Y|Ys], [(X,Y)|Zs]) :- zip(Xs,Ys,Zs).
X ∈ Γ :- member(X, Γ). % 要素を順番に取り出す

new(_).

% 型変数検査と変数検査
tVar(X) :- var(X).
val(X) :- atom(X).

fv(X      ,[X]) :- tVar(X), !.
fv(_!Ts     ,R) :- !,maplist(fv,Ts,Ts_), foldr(union_eq,Ts_,[],R),!.
fv((T1->T2) ,R) :- !,maplist(fv,[T1,T2],Ts_), foldr(union_eq,Ts_,[],R),!.
fv(∀(X,_,T),R) :- !,fv(T,Ts), subtract_eq(Ts,[X],R).
fv(_       ,[]) :- !.

sub(St,X,R)                  :- var(X),(X1,T)∈St,X==X1,!,sub(St,T,R).
sub(_,X,X)                   :- var(X),!.
sub(St,O!Ts,O!R)             :- maplist(sub(St),Ts,R).
sub(St,(T1->T2),(T1_->T2_))  :- sub(St,T1,T1_),sub(St,T2,T2_).
sub(St,∀(X,S,T),∀(X,S,T_)) :- sub(St,T,T_).
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(G1,Env,T1,(G_,T_)) :- fv(T1,Fv1),efv(Env,EFv),
                          subtract_eq(Fv1, EFv, Ans),
                          gsubtract(G1,Ans,G_),
                          foldr(gen1(G1),Ans,T1,T_).
gen1(G1,An,T,∀(An,R,T))   :- gapp(G1,An,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)) :- tVar(T).
inst(∀(An,Sn,T),G,TG):- !,new(Bn),log(1,new(Bn)),
                              sub([(An,Bn)],T,T1),log(1,sub([(An,Bn)],T,T1)),
                              gunion(G,[(Bn,Sn)],G1),
                              log(1,gunion(G,[(Bn,Sn)],G1)),
                              inst(T1,G1,TG).
inst(T,G,(T,G)).

%mgu(T1,T2, _) :- log(app,mgu(T1,T2)),fail.
mgu(T1,T2,[]) :- T1==T2,!.
mgu(A,T,[(A,T)]) :- tVar(A),!.
mgu(T,A,[(A,T)]) :- tVar(A),!.
mgu(X1!Ts1,X2!Ts2,R) :- X1==X2,!,zip(Ts1,Ts2,Ts), foldl(mgu1,Ts,[],R).
mgu((T1->T2),(T3->T4),R) :- !,foldl(mgu1,[(T1,T3),(T2,T4)],[],R).
mgu(T1,T2,_) :- failwith('mgu error ~w ~w',[T1,T2]).
%mgu1(T,St,_) :- log(app,mgu1(St,T)),fail.
mgu1((T1,T2),St,R):- sub(St,T1,T1_),sub(St,T2,T2_),
                     mgu(T1_,T2_,St_),union_eq(St, St_,R),!.

%unify(G,T1,T2, _) :- log(app,unify(G,T1, T2)),fail.
unify(G,D,T1,T2,G_) :- mgu(T1,T2,St), !,stdom(St,DomAs),!, %mguした置換ドメインで単一化ハンドリング
                       foldr(unify1(St,G,D),DomAs,[],Gc),
                       gsubtract(G,DomAs,G2),%古いの捨てて
                       gunion(Gc,G2,G_),
                       maplist([(A,A)]>>!,St).% 新しいのを追加する
unify1(St,G,D,A,Gc,Gc_):- gapp(G,A,Ga), % 単一化された型変数の制約を取り出し
                          sub(St,A,A_), % 置換
                          constrain(A_,Ga,D,G_), % 制約を処理
                          gunion(Gc,G_,Gc_). % 制約追加
constrain(_,(A,S),G,G_) :- tVar(A),gunion([(A,S)],G,G_). % 型変数なら 制約を伝搬
constrain(K!Ts,D,S,G3) :- foldr(constrain1(K!Ts,D),S,[],G3). % 型コンストラクタをソート(中身は型クラス名)でループ
constrain(_,_,_,[]).
constrain1(K!Ts,D,C,G,G_) :- kcdom((K,C),D,Ss),constr(Ts,Ss,G2),gunion(G2,G,G_).% それぞれの引数の制約取り出して処理
constr(Ts,Ss,G3) :- zip(Ts,Ss,Tss), foldr(constr1,Tss,[],G3).
constr1((Ti,Si),G,G2) :- constrain(Ti,Si,G1), gunion(G,G1,G2).
stdom(St,As) :- foldr(stdom1(St),St,[],As).
stdom1(St,(A,_),As,[A|As]) :- sub(St,A,A1), A==A1.
stdom1(_,_,As,As).
kcdom((K,C),D,Ss) :- inst(K,Ss,C) ∈ D. % インスタンス宣言時のソートリストがドメイン

i(λ(X,E),G,D,Env,((A->T),G_)):- new(A),i(E,G,D,[(X,A)|Env],(T,G_)).
i(let X=E1;E2,G,D,Env,R)   :- !,log(1,letok1),i(E1,G,D,Env,(T1,G1)),
                              log(1,letok2),
                              gen(G1,Env,T1,(G_,T_)),!,
                              log(1,letok3;gen(G1,Env,T1,(G_,T_))),!,
                              log(1,i(E2,G_,D,[(X,T_)|Env])),!,
                              i(E2,G_,D,[(X,T_)|Env],R),
                              log(1,letok4;R),!.
i(X,G,_,Env,(T_,G_))    :- val(X),!,
                           (X1,T)∈Env,X1==X,log(1,X:T),
                           inst(T,G,(T_,G_)),log(1,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)),
                            new(A),
                            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) :- new(X).

tp(I,St, Env, E, T_) :- reset,
  log(1,'test ~i\n',[E]),
  maplist([(A,A)]>>true,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,!).

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).

np93btest.pl

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

:- begin_tests(foldr).

  test(foldl0) :- foldl(concat,[a,b,c],'',cba).
  test(foldr0) :- foldr(concat,[a,b,c],'',abc).

:- end_tests(foldr).

pair(Xs,(A,B)) :- select(A,Xs,Ys),select(B,Ys,_).
dim(Xs) :- forall(member(C,Xs),var(C)),forall(pair(Xs,(A,B)),dif(A,B)).

:- begin_tests(fv).
  test('fv x') :- fv(X,R),R==[X].
  test('fv type constructor') :- fv(x![Y,Z],R),R==[Y,Z].
  test('fv array') :- fv((X->Y),R),R==[X,Y].
  test('fv forall') :- fv(∀(X,[],(D->X->Y)),R),R==[D,Y].
  test('fv forall2') :- fv(∀(Y,[],∀(X,[],(D->X->Y))),R),R==[D].
  test('fv forall_pia') :- fv(∀(X,['Eq','Ord'],(D->X)),R),R==[D]. % todo
  test('fv int') :- fv(int,R),R==[].
:- end_tests(fv).

:- begin_tests('mono').
  test('mono int')        :- tp1(1,R),R==int.
  test('mono float')      :- tp1(1.0,R),R==float.
  test('mono let')        :- tp1(let x=1;x,R),R==int.
  test('mono lambda id')  :- tp1(λ(x,x),R),R= ∀(x0,[], (x0 -> x0)).
  test('mono let id')     :- tp1(let id=λ(x,x); id,R),R= ∀(x1,[],(x1->x1)).
  test('mono let id app') :- tp1(let id=λ(x,x); id $ 1,int).
:- end_tests('mono').

:- begin_tests('poly').
  test('let _=id int;id float'):-
    tp1(let id=λ(x,x); let a= id $ 1; id$1.0,float).
  test('id id'):- tp1(let id=λ(x,x); id$id,R),R= ∀(x2,[],(x2->x2)).
  test('id id 1'):- tp1(let id=λ(x,x); id$id$1,R),R=int.
:- end_tests('poly').

:- begin_tests('type constructor').

  test('a:int'):- tp3([],[(a, int)],  a, int).
  test('a:f'):- tp3([],[(a, float)],  a, float).

  test('mkp f:f') :- tp3([],[(mkPoint, float)], mkPoint, float).
  test('mkp f f:f->f->p') :-
    tp3([],[(mkPoint, (float->float->Point))],mkPoint,(float->float->Point)).
  test('p=p!();mkp:f->p;mk 2.0:p!()') :-
          tp3([(Point, 'Point'![])],
          [(mkPoint, (float->Point))],
          mkPoint $ 2.0, 'Point'![]).
  test('p=p!();mkp:f->f->p;mkp 2. 3.:p!()') :-
    tp3([(Point, 'Point'![])],
        [(mkPoint, (float->float->Point))],
        mkPoint $ 2.0 $ 3.0,'Point'![]).
  test('p=p!();mkp:f->f->p;let') :-
    tp3([(Point, 'Point'![])],
        [(mkPoint, (float->float->Point))],
        let p = mkPoint $ 2.0 $ 3.0; p, 'Point'![]).
  test('p=p!();pt1 p + pt2 p') :-
    tp3([(Point, 'Point'![])],
        [
          (mkPoint, (float->float->Point)),
          (pt1, (Point->float)),
          (pt2, (Point->float)),
          (+, (float->float->float))
        ],
        let p = mkPoint $ 2.0 $ 3.0;
        (+)$(pt1 $ p)$(pt2 $ p),
        float).

:- end_tests('type constructor').

:- begin_tests('kcdom').
  test(dom1) :- \+kcdom(('Pt',[]),[inst('Pt',[],'Eq')],[]).
    test(dom2) :- kcdom(('Pt','Eq'),[inst('Pt',[['Eq']],'Eq')],[['Eq']]).
    test(dom2) :- kcdom(('Pt','List'),[inst('Pt',[['Eq'],['Ord']],'List')],[['Eq'],['Ord']]).
:- end_tests('kcdom').

:- begin_tests('inst').

  test('class Xcoord;xcoord') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->Point)),
         (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        xcoord
      ,R), R = ∀(x0,['Xcoord'],(x0->float)).

  test('class Xcoord;inst Point Xcoord; 2.0') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->Point)),
          (ptx, (Point->float))],
        class('Xcoord', xcoord, ∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        2.0
      ,float).

  test('class Xcoord;inst Point Xcoord;xcoord $ mkp 2.0') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->Point)),
          (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        xcoord $(mkPoint $ 2.0)
      ,float).
  test('inst P xcd;inst P3d;xcd P') :-
      tpp([
          (Point, 'Point'![]),
          (Point3D, 'Point3D'![])
        ],
        [
          (mkPoint, (float->Point)),
          ('MkPoint3D', (float->Point3D)),
          (pt3dx, (Point3D->float)),
          (ptx, (Point->float))
          ],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        inst('Point3D',[],'Xcoord', xcoord, λ(u, pt3dx $ u));
        let p = mkPoint $ 10.0;
        xcoord $ p
        ,float).
  test('inst P xcd;inst P3d;xcd P3d') :-
    tpp([
          (Point, 'Point'![]),
          (Point3D, 'Point3D'![])
        ],
        [
          (mkPoint, (float->Point)),
          ('MkPoint3D', (float->Point3D)),
          (pt3dx, (Point3D->float)),
          (ptx, (Point->float))
        ],
        (class('Xcoord',xcoord, ∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        inst('Point3D',[],'Xcoord', xcoord, λ(u, pt3dx $ u));
        let p3 = 'MkPoint3D' $ 10.0;
        xcoord $ p3)
        ,float).

  test('inst P xcd;inst P3d;xcd P+xcd P3d') :-
    tpp([
          (Point, 'Point'![]),
          (Point3D, 'Point3D'![])
        ],
        [
          (mkPoint, (float->Point)),
          (ptx, (Point->float)),
          ('MkPoint3D', (float->Point3D)),
          (pt3dx, (Point3D->float)),
          ((+.), (float->float->float))
        ],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        inst('Point3D',[],'Xcoord', xcoord, λ(u, pt3dx $ u));
        let p = mkPoint $ 2.0;
        let p3 = 'MkPoint3D' $ 10.0;
        (+.)$( xcoord $p)$( xcoord $p3),
      float).

:- end_tests('inst').

:- begin_tests('dict').

  test('id') :-
    tp3([],[],let a=λ(u,u);a,∀(x1,[],(x1->x1))).
  test('class Xcd;inst P Xcd;xcd') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->float->Point)),
          (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        xcoord,
      ∀(x0,['Xcoord'],(x0->float))).
  test('class Xcd;inst P Xcd;λp.xcd') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->float->Point)),
         (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        λ(p,xcoord)
      ,∀(x0,[],∀(x1,['Xcoord'],(x0->x1->float)))).
  test('class Xcd;inst P Xcd;let a=xcd;a') :-
    tpp([(Point, 'Point'![])],
        [(mkPoint, (float->float->Point)),
         (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        let a=xcoord;a
      ,∀(x1,['Xcoord'],(x1->float))).

  test('class Xcd;inst P Xcd;let x=λp.xcd p;xx p') :-
    tpp([(Point, 'Point'![])],
        [ (mkPoint, (float->float->Point)),
          (ptx, (Point->float))],
        class('Xcoord',xcoord,∀(A,['Xcoord'],(A->float)));
        inst('Point',[],'Xcoord', xcoord, λ(u, ptx $ u));
        let xx = λ(p, xcoord $ p);
        let p = mkPoint $ 2.0 $ 3.0;
        xx $ p
      ,float).

  test('let dst=λp.xcd p+ycd p;dst cpt') :-
    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)),
        (add, (float->float->float)),
        (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).

:- end_tests('dict').

:- begin_tests('param').
  test('pt') :-
    tpp([],
      [ (point, ∀(A,[],(A->'Point'![A])))],
      point $ 1,
    'Point'![int]).

  test('ptx $ pt 1') :-
    tpp([],
      [ (point, ∀(A,[],(A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->A)))
        ],
      ptx $ (point $ 1),
    int).

  test('data P a = P a;class Xcd;inst Xcd; 1') :-
    tpp([],
      [ ('point', ∀(A,[],(A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->A)))
        ],
      class('Xcoord',xcoord,∀(A,['Xcoord'],∀(B,[],(A->B))));
      inst('Point',[[]],'Xcoord', xcoord, λ(u, ptx $ u));
      1
    ,int).

  test('data P a = P f a;class Xcd;inst P Xcd;xcd $ P 1.2 1') :-
    tpp([],
      [ ('point', ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float)))
        ],
      class('Xcoord',xcoord,∀(B,['Xcoord'], (B->float)));
      inst('Point',[[]],'Xcoord', xcoord, λ(u,ptx $ u));
      xcoord $ ('point' $ 1.2 $ 1),
    float).
  test('data P a = P f a;class Xcd;inst P Xcd;xcd $ P 1.2 1') :-
    tpp([],
      [ ('Point', ∀(A,[],(float->A->'Point'![A])))],
      class('Id',id,∀(B,['Id'], (B->B)));
      inst('Point',[[]],'Id', id, λ(u,u));
      id $ ('Point' $ 1.2 $ 1),
    'Point'![int]).

  test('data P a = P f a;class Id;inst P Id;id $ P 1.2 1.1') :-
    tpp([],
      [ ('Point', ∀(A,[],(float->A->'Point'![A]))) ],
      class('Id',id,∀(B,['Id'], (B->B)));
      inst('Point',[[]],'Id', id, λ(u,u));
      id $ ('Point' $ 1.2 $ 1.1),
    'Point'![float]).

:- end_tests('param').

:- begin_tests('sorts').
  test('data P a = P f a;class Xcd;inst P Xcd;xcd $ P 1.2 1') :-
    tpp([],
      [ ('point', ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float)))
        ],
      class('Xcoord',xcoord,∀(B,['Xcoord'], (B->float)));
      inst('Point',[[]],'Xcoord', xcoord, λ(u,ptx $ u));
      xcoord $ ('point' $ 1.2 $ 1),
    float).

  test('data P a = P f a;class Eq;class Xcd;inst P Eq;inst P(Eq)Xcd; xcd $ P 1.2 1') :-
    tpp([],
      [ ('point', ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float))),
        (pteq, ∀(A,[],('Point'![A]->'Point'![A]->int)))
      ],
        class('Eq',eq,∀(B,['Eq'], (B->B->int)));
        class('Xcoord',xcoord,∀(B,['Xcoord'], (B->float)));
        inst('Point',[[]],'Eq', eq, λ(u,pteq $ u));
        inst('Point',[['Eq']],'Xcoord', xcoord, λ(u,ptx $ u));
      xcoord $ ('point' $ 1.2 $ 1)
    ,float).

:- end_tests('sorts').

:- begin_tests('extends').
  test('data P a = P f a;class Eq;inst P Eq;class Xcd<:Eq;inst P Xcd; xcd $ P 1.2 1') :-
    tpp([],
      [ ('point', ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float))),
        (pteq, ∀(A,[],('Point'![A]->'Point'![A]->int)))
        ],
      class('Eq',eq,∀(B,['Eq'], (B->B->int)));
      inst('Point',[[]],'Eq', eq, pteq);
      class('Xcoord',xcoord,∀(B,['Xcoord','Eq'], (B->float)));
      inst('Point',[[]],'Xcoord', xcoord, λ(u,ptx $ u));
      xcoord $ ('point' $ 1.2 $ 1)
    ,float).
  test('error class Eq;class Xcd<:Eq;inst P Xcd; xcd $ P 1.2 1') :-
    tpp([],
      [ ('point', ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float))),
        (pteq, ∀(A,[],('Point'![A]->'Point'![A]->int)))
        ],
      class('Eq',eq,∀(B,['Eq'], (B->B->int)));
      class('Xcoord',xcoord,∀(B,['Xcoord','Eq'], (B->float)));
      inst('Point',[[]],'Xcoord', xcoord, λ(u,ptx $ u));
      xcoord $ ('point' $ 1.2 $ 1),
   error).
  test('error class Eq;class List<:Eq;inst P List; single $ P 1.2 1') :-
    tpp([],
      [ (point, ∀(A,[],(float->A->'Point'![A]))),
        (ptx, ∀(A,[],('Point'![A]->float))),
        (pteq, ∀(A,[],('Point'![A]->'Point'![A]->int)))
        ],
      class('Eq',eq,∀(B,['Eq'], (B->B->int)));
      class('List',single,∀(B,['List','Eq'], (B->float)));
      inst('Point',[[]],'List', single, λ(u,ptx $ u));
      xcoord $ (point $ 1.2 $ 1),
   error).

:- end_tests('extends').
/**/
:- run_tests.
:- halt.