fork(1) download 
  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.  
  12. type(KC,C,var(X),     T1) --> { first(X:T,C) }, inst_type(KC,T,T1).
  13. type(KC,C,lam(X,E), A->B) --> type(KC,[X:mono(A)|C],E,B), [kind(KC,A->B,o)].
  14. type(KC,C,X $ Y,       B) --> type(KC,C,X,A->B), type(KC,C,Y,A).
  15. type(KC,C,let(X=E0,E1),T) --> type(KC,C,E0,A), type(KC,[X:poly(C,A)|C],E1,T).
  16.  
  17. first(X:T,[X1:T1|_]) :- X = X1, T = T1.
  18. first(X:T,[X1:_|Zs]) :- X\==X1, first(X:T, Zs).
  19.  
  20. instantiate(mono(T),T).
  21. instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).
  22.  
  23. inst_type(KC,poly(C,T),T2) -->
  24.   { copy_term(t(C,T),t(C,T1)), 
  25.     free_variables(T,Xs), free_variables(T1,Xs1) }, % Xs and Xs1 are same length
  26.   samekinds(KC,Xs,Xs1), { T1=T2 }. %% unify T1 T2 later (T2 might not be var)
  27. inst_type(_ ,mono(T),T) --> [].
  28.  
  29. samekinds(KC,[X|Xs],[Y|Ys]) --> { X\==Y }, [kind(KC,X,K),kind(KC,Y,K)],
  30.                                 samekinds(KC,Xs,Ys).
  31. samekinds(KC,[X|Xs],[X|Ys]) --> [], samekinds(KC,Xs,Ys).
  32. samekinds(_ ,[],[]) --> [].
  33.  
  34. variablize(var(X)) :- gensym(t,X).
  35.  
  36. main:-
  37. 	process,
  38. 	halt.
  39.  
  40. type_and_print(KC,C,E,T) :-
  41.   phrase(type(KC,C,E,T),Gs),
  42.   (bagof(Ty, X^Y^member(kind(X,Ty,Y),Gs), Tys); Tys=[]),
  43.   free_variables(Tys,Xs), maplist(variablize,Xs), maplist(call,Gs),
  44.   write("kind ctx instantiated as: "), print(KC), nl, print(E : T), nl.
  45.  
  46. process:-
  47. 	/* your code goes here */
  48. 	type_and_print(_,[],lam(x,var(x)),_), nl,
  49. 	type_and_print(_,[],lam(x,lam(y,var(y)$var(x))),_), nl,
  50. 	type_and_print(_,[],let(id=lam(x,var(x)),var(id)$var(id)),_), nl,
  51. 	KC0 =
  52. 	 [ 'Nat':mono(o)
  53.      , 'List':mono(o->o)
  54.      ],
  55. 	Nat = var('Nat'), List = var('List'),
  56.     C0 =
  57.      [ 'Zero':mono(Nat)
  58.      , 'Succ':mono(Nat -> Nat)
  59.      , 'Nil' :poly([], List$A)
  60.      , 'Cons':poly([], A->((List$A)->(List$A)))
  61.      ],
  62.     append(KC0,_,KC1),
  63.     type_and_print(KC1,C0,lam(x,lam(n,var(x)$var('Succ')$var(n))),_),
  64. 	true.
  65.  
  66. %% haven't really shown examples of type constructor polymorphsim or
  67. %% kind polymorphism here but you get the idea what strucutural extensions
  68. %% to HM are needed to support type constructor and kind polymoprhisms
  69.  
  70. :- main.
Success #stdin #stdout 0.03s 7928KB
comments (?)
stdin 
Standard input is empty
stdout 
kind ctx instantiated as: [t1:mono(o)|_G1601]
lam(x,var(x)): (var(t1)->var(t1))

kind ctx instantiated as: [t2:mono(o),t3:mono(o)|_G1840]
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)|_G2231]
let(id=lam(x,var(x)),var(id)$var(id)): (var(t5)->var(t5))

kind ctx instantiated as: ['Nat':mono(o),'List':mono((o->o)),t6:mono(o),t7:mono(o)|_G2606]
lam(x,lam(n,var(x)$var('Succ')$var(n))): (((var('Nat')->var('Nat'))->var(t6)->var(t7))->var(t6)->var(t7))
https://ideone.com/q44ufk
HM, type constructor poly, kind poly using Prolog
language:
Prolog (swi 7.6.4)
created:
8 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!