fork download
copy 
  1. :- set_prolog_flag(verbose,silent).
  2. :- prompt(_, '').
  3. :- use_module(library(readutil)).
  4.  
  5. :- set_prolog_flag(occurs_check,true).
  6. :- op(500,yfx,$).
  7.  
  8. kind(KC,var(Z),K1) :- first(Z:K,KC), instantiate(K,K1).
  9. kind(KC,F $ G, K2) :- kind(KC,F,K1 -> K2), kind(KC,G,K1).
  10. kind(KC,A -> B,o)  :- kind(KC,A,o), kind(KC,B,o).
  11. kind(KC,mu(F), K)  :- kind(KC,F,K->K).
  12.  
  13. type(KC,C,var(X),     T1) --> { first(X:T,C) }, inst_type(KC,T,T1).
  14. type(KC,C,lam(X,E), A->B) --> type(KC,[X:mono(A)|C],E,B), [kind(KC,A->B,o)].
  15. type(KC,C,X $ Y,       B) --> type(KC,C,X,A->B), type(KC,C,Y,A).
  16. type(KC,C,let(X=E0,E1),T) --> type(KC,C,E0,A), type(KC,[X:poly(C,A)|C],E1,T).
  17. type(KC,C,in(N,E),     T) --> type(KC,C,E,T0),
  18.                               { unfold_N_ap(1+N,T0,F,[mu(F)|Is]),
  19.                                 foldl_ap(mu(F),Is,T) }.
  20. %%%%% Alts is a pattern lambda. (Alts $ E) is "case E of Alts" in Haskell
  21. type(KC,C,     Alts,A->T) --> type_alts(KC,C,Alts,A->T), [kind(KC,A->T,o)].
  22.  
  23. type(KC,C,mit(X,Alts),mu(F)->T) -->
  24.   { is_list(Alts), gensym(r,R),
  25.     KC1 = [R:mono(o)|KC], C1 = [X:poly(C,var(R)->T)|C] },
  26.   type_alts(KC1,C1,Alts,F$var(R)->T).
  27.  
  28. type(KC,C,mit(X,Is-->T0,Alts),A->T) -->
  29.   { is_list(Alts), gensym(r,R),
  30.     foldl_ap(mu(F),Is,A), foldl_ap(var(R),Is,RIs),
  31.     KC1 = [R:mono(K)|KC], C1 = [X:poly(C,RIs->T0)|C] },
  32.   [kind(KC,F,K->K), kind(KC,A->T,o)], % delayed goals
  33.   { foldl_ap(F,[var(R)|Is],FRIs) },
  34.   type_alts(KC1,C1,Alts,FRIs->T).
  35.  
  36.  
  37. type_alts(KC,C,[Alt],          A->T) --> type_alt(KC,C,Alt,A->T).
  38. type_alts(KC,C,[Alt,Alt2|Alts],A->T) --> type_alt(KC,C,Alt,A->T),
  39.                                          type_alts(KC,C,[Alt2|Alts],A->T).
  40.  
  41. type_alt(KC,C,P->E,A->T) --> % assume single depth pattern (C x0 .. xn)
  42.   { P =.. [Ctor|Xs], upper_atom(Ctor),
  43.     findall(var(X),member(X,Xs),Vs),
  44.     foldl_ap(var(Ctor),Vs,PE),% PE=var('Cons')$var(x)$var(xs) when E='Cons'(x,xs)
  45.     findall(X:mono(_),member(X,Xs),C1,C) }, % C1 extends C with bindings for Xs
  46.   type(KC,C1,PE,A), type(KC,C1,E,T).
  47.  
  48. % assume upper atoms are tycon or con names and lower ones are var names
  49. upper_atom(A) :- atom(A), atom_chars(A,[C|_]), char_type(C,upper).
  50. lower_atom(A) :- atom(A), atom_chars(A,[C|_]), char_type(C,lower).
  51.  
  52. unfold_N_ap(0,E,    E,[]).
  53. unfold_N_ap(N,E0$E1,E,Es) :-
  54.   N>0, M is N-1, unfold_N_ap(M,E0,E,Es0), append(Es0,[E1],Es).
  55.  
  56. foldl_ap(E, []     , E).
  57. foldl_ap(E0,[E1|Es], E) :- foldl_ap(E0$E1, Es, E).
  58.  
  59.  
  60.  
  61. first(X:T,[X1:T1|_]) :- X = X1, T = T1.
  62. first(X:T,[X1:_|Zs]) :- X\==X1, first(X:T, Zs).
  63.  
  64. instantiate(mono(T),T).
  65. instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).
  66.  
  67. inst_type(KC,poly(C,T),T2) -->
  68.   { copy_term(t(C,T),t(C,T1)), 
  69.     free_variables(T,Xs), free_variables(T1,Xs1) }, % Xs and Xs1 are same length
  70.   samekinds(KC,Xs,Xs1), { T1=T2 }. %% unify T1 T2 later (T2 might not be var)
  71. inst_type(_ ,mono(T),T) --> [].
  72.  
  73. samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y }, [kind(KC,X,K),kind(KC,Y,K)],
  74.                                 samekinds(KC,Xs,Ys).
  75. samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).
  76. samekinds(_ ,[],[]) --> [].
  77.  
  78. variablize(var(X)) :- gensym(t,X).
  79.  
  80. main:-
  81. 	process,
  82. 	halt.
  83.  
  84. type_and_print(KC,C,E,T) :-
  85.   phrase(type(KC,C,E,T),Gs),
  86.   (bagof(Ty, X^Y^member(kind(X,Ty,Y),Gs), Tys); Tys=[]),
  87.   free_variables(Tys,Xs), maplist(variablize,Xs), maplist(call,Gs),
  88.   write("kind ctx instantiated as: "), print(KC), nl, print(E : T), nl.
  89.  
  90. process:-
  91. 	/* your code goes here */
  92. 	type_and_print(_,[],lam(x,var(x)),_), nl,
  93. 	type_and_print(_,[],lam(x,lam(y,var(y)$var(x))),_), nl,
  94. 	type_and_print(_,[],let(id=lam(x,var(x)),var(id)$var(id)),_), nl,
  95. 	KC0 =
  96. 	 [ 'N':mono(o->o)
  97.      , 'L':mono(o->o->o)
  98.      , 'B':mono((o->o)->(o->o))
  99.      ],
  100.     C0 =
  101.      [ 'Z':poly([] , N$R1)
  102.      , 'S':poly([] , R1 -> N$R1)
  103.      , 'N':poly([] , L$A2$R2)
  104.      , 'C':poly([] , A2->(R2->(L$A2$R2)))
  105.      , 'BN':poly([] , B$R3$A3)
  106.      , 'BC':poly([] , A3 -> R3$(R3$A3) -> B$R3$A3)
  107.      , 'plus':poly([], mu(N) -> mu(N) -> mu(N))
  108.      %% , 'undefined':poly([], X1231245424)
  109.      ],
  110.     N = var('N'), L = var('L'), B = var('B'),
  111. % data B r a = BN | BC a (r(r a))
  112. % B : (* -> *) -> (* -> *)
  113. % BN: B r a
  114. % BC: a -> r(r a) -> B r a
  115.     X = var(x), Y = var(y), W = var(w),
  116.     Z = var('Z'), S = var('S'),
  117.     Zero=in(0,Z), Succ=lam(x,in(0,S$X)),
  118.     N = var('N'), C = var('C'),
  119.     Nil=in(0,N), Cons=lam(x,lam(xs,in(0,C$X$var(xs)))),
  120.     BN = var('BN'), BC = var('BC'),
  121.     BNil=in(1,BN), BCons=lam(x,lam(xs,in(1,BC$X$var(xs)))),
  122.     TM_id = lam(x,X),
  123.     TM_S = lam(x,lam(y,lam(w,(X$W)$(Y$W)))),
  124.     TM_bad = lam(x,X$X),
  125.     TM_e1 = let(id=TM_id,var(id)$var(id)),
  126.     TM_e2 = lam(y,let(x=lam(w,Y),X$X)),
  127.     TM_e3a = (C$Zero$Nil),
  128.     TM_e3f = ['N'->Zero,'C'(x,xs)->X], %% $ (C$Zero$Nil),
  129.     TM_e3 = ['N'->Zero,'C'(x,xs)->X] $ (C$Zero$Nil),
  130.     TM_lendumb0 = mit(len,['N'->Zero]),
  131.     TM_lendumb = mit(len,['N'->Zero,'C'(x,xs)->Zero]),
  132.     TM_len = mit(len,['N'->Zero,'C'(x,xs)->Succ$(var(len)$var(xs))]),
  133.     %% length of list example
  134.     TM_e4 = let(length=TM_len, Cons$ (var(length)$(Cons$Zero$Nil))
  135.                                    $ (Cons$ (var(length)$(Cons$Nil$Nil)) $ Nil) ),
  136.     %% sum of bush example
  137.     TM_e5 = mit(bsum, [I]-->((I->mu(N))->mu(N)),
  138.                [ 'BN'       -> lam(f,Zero)
  139.                , 'BC'(x,xs) -> lam(f,
  140.                      var(plus) $ (var(f)$X)
  141.                                $ (var(bsum) $ var(xs)
  142.                                             $ lam(ys,var(bsum)$var(ys)$var(f)) )
  143.                                   )
  144.                ]),
  145.     append(KC0,_,KC1), copy_term(C0,C1),
  146.     type_and_print(KC1,C1,lam(x,lam(n,X$Succ$var(n))),_), nl, !,
  147.     append(KC0,_,KC2), copy_term(C0,C2),
  148.     type_and_print(KC2,C2,TM_e3,_), nl, !,
  149.     append(KC0,_,KC3), copy_term(C0,C3),
  150.     type_and_print(KC3,C3,TM_len,_), nl, !,
  151.     append(KC0,_,KC4), copy_term(C0,C4),
  152.     type_and_print(KC4,C4,TM_e4,_), nl, !,
  153.     append(KC0,_,KC5), copy_term(C0,C5),
  154.     type_and_print(KC5,C5,TM_e5,_), nl, !,
  155.     true.
  156.  
  157. %% haven't really shown examples of type constructor polymorphsim or
  158. %% kind polymorphism here but you get the idea what strucutural extensions
  159. %% to HM are needed to support type constructor and kind polymoprhisms.
  160.  
  161. %% At this level, the examples are complex enough. So downloading it and
  162. %% running it on your local SWI-Prolog may be more pleasant to experiment.
  163. %% You may also want a parser and pretty printer for micronax language.
  164.  
  165. :- main.
Success #stdin #stdout #stderr 0.04s 8016KB
comments (?)
stdin
copy 
Standard input is empty
stdout
copy 
kind ctx instantiated as: [t1:mono(o)|_G340]
lam(x,var(x)): (var(t1)->var(t1))

kind ctx instantiated as: [t2:mono(o),t3:mono(o)|_G579]
lam(x,lam(y,var(y)$var(x))): (var(t2)-> (var(t2)->var(t3))->var(t3))

kind ctx instantiated as: [t4:mono(o),t5:mono(o)|_G970]
let(id=lam(x,var(x)),var(id)$var(id)): (var(t5)->var(t5))

kind ctx instantiated as: ['N':mono((o->o)),'L':mono((o->o->o)),'B':mono(((o->o)->o->o)),t6:mono(o),t7:mono(o),t8:mono(o)|_G2002]
lam(x,lam(n,var(x)$lam(x,in(0,var('S')$var(x)))$var(n))): (((mu(var('N'))->mu(var('N')))->var(t7)->var(t8))->var(t7)->var(t8))

kind ctx instantiated as: ['N':mono((o->o)),'L':mono((o->o->o)),'B':mono(((o->o)->o->o)),t9:mono(o),t10:mono(o),t11:mono(o),t12:mono(o)|_G3744]
[ ('N'->in(0,var('Z'))), ('C'(x,xs)->var(x))]$ (var('C')$in(0,var('Z'))$in(0,var('N'))):mu(var('N'))

kind ctx instantiated as: ['N':mono((o->o)),'L':mono((o->o->o)),'B':mono(((o->o)->o->o)),t13:mono(_G4366),t14:mono(_G4366),t15:mono(o),t16:mono(o)|_G5447]
mit(len,[ ('N'->in(0,var('Z'))), ('C'(x,xs)->lam(x,in(0,var('S')$var(x)))$ (var(len)$var(xs)))]): (mu(var('L')$var(t14))->mu(var('N')))

kind ctx instantiated as: ['N':mono((o->o)),'L':mono((o->o->o)),'B':mono(((o->o)->o->o)),t17:mono(o),t18:mono(o),t19:mono(o),t20:mono(o),t21:mono(o)|_G11699]
let(length=mit(len,[ ('N'->in(0,var('Z'))), ('C'(x,xs)->lam(x,in(0,var('S')$var(x)))$ (var(len)$var(xs)))]),lam(x,lam(xs,in(0,var('C')$var(x)$var(xs))))$ (var(length)$ (lam(x,lam(xs,in(0,var('C')$var(x)$var(xs))))$in(0,var('Z'))$in(0,var('N'))))$ (lam(x,lam(xs,in(0,var('C')$var(x)$var(xs))))$ (var(length)$ (lam(x,lam(xs,in(0,var('C')$var(x)$var(xs))))$in(0,var('N'))$in(0,var('N'))))$in(0,var('N')))):mu(var('L')$mu(var('N')))

kind ctx instantiated as: ['N':mono((o->o)),'L':mono((o->o->o)),'B':mono(((o->o)->o->o)),t22:mono(o),t23:mono((o->o)),t24:mono(o),t25:mono(o)|_G14326]
mit(bsum, ([var(t22)]--> (var(t22)->mu(var('N')))->mu(var('N'))),[ ('BN'->lam(f,in(0,var('Z')))), ('BC'(x,xs)->lam(f,var(plus)$ (var(f)$var(x))$ (var(bsum)$var(xs)$lam(ys,var(bsum)$var(ys)$var(f)))))]): (mu(var('B'))$var(t22)-> (var(t22)->mu(var('N')))->mu(var('N')))
stderr
copy 
Warning: /home/PhTnZd/prog:90:
	Singleton variables: [BNil,BCons,TM_S,TM_bad,TM_e1,TM_e2,TM_e3a,TM_e3f,TM_lendumb0,TM_lendumb]
https://ideone.com/Iv52Y5
HM, tycon poly, kind poly, (non-nested) pattern matching, Mendler-style recursion schemes over algebraic data types using Prolog
language:
Prolog (swi 7.6.4)
created:
7 years ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!