3 ms·

Prolog variables are metavariables, if you use them as such. ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ). Typ = [_G947, _G948]^ ((_G947->_

Prolog variables are metavariables, if you use them as such. ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ). Typ = [_G947, _G948]^ ((_G947->_G948)->_G947->_G948) . ?- abstract_type(lambda(f, lambda(g, apply(f, g))), Typ), apply_type(Typ, a, Ta), apply_type(Ta, b, Tab), apply_type(Typ, c, Tc), apply_type(Tc, d, Tcd). Typ = [_G1179, _G1180]^ ((_G1179->_G1180)->_G1179->_G1180), Ta = [_G1213]^ ((a->_G1213)->a->_G1213), Tab = ((a->b)->a->b), Tc = [_G1251]^ ((c->_G1251)->c->_G1251), Tcd = ((c->d)->c->d) . Note how both Tab and Tcd arise from instantiating the same schema Typ, which is unchanged. To avoid binding variables in the schema, you just make sure to only instantiate instances (copies) of the schema: abstract_type(Term, Typ) :- type(Term, [], T), % type/3 defined by parent term_variables(T, Vars), Typ = Vars^T. apply_type(Typ, Arg, Result) :- copy_term(Typ, TypCopy), TypCopy = Vars^T, Vars = [Arg | RemainingVars], ( RemainingVars = [] -> Result = T ; Result = RemainingVars^T ).

junke 9y ago
Thanks! Just to expand on my previous example, I can simply modify how bindings are looked up and generalize the associated type when it is not unknown: type(V,Env,T) :- ground(V), member(V:P,Env), generalize(P,T). generalize(P,T) :- nonvar(P), !, copy_term(P,T). generalize(T,T). Let's add two rules for tuples and addition, and change the syntax of let for clarity: type((A,B),Env,TA * TB) :- type(A,Env,TA), type(B,Env,TB). type(A+B,Env,number) :- type(A,Env,number), type(B,Env,number). type(let(X == XE, E),Env,ET) :- type(XE,Env,XT), type(E,[X:XT|Env],ET). Then, typing this: let(identity == lambda(v,v), let(increment == lambda(x,x+1), let(compose == lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))), (apply(apply(compose,identity),identity), apply(apply(compose,increment),increment))))) ... gives: (_1775 -> _1775) * (number -> number) You could also make use of meta attributes, ie. data stored inside variables, to control what happens during unification.
psygnisfive 9y ago
mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!
- tom_mellior 9y ago
  That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate the quantification, I then just add that list in front of the term with the ^ operator (which has no semantics, it is just the traditional constructor for these things). So for `_G947 -> _G947` I get the variable list `[_G947]` and use it to represent the universally quantified term as `[_G947]^(_G947 -> _G947)`. If you want to display this with nicer variable names, just substitute names of your choice for the variables in the quantifier list.

junke 9y ago

Thanks! Just to expand on my previous example, I can simply modify how bindings are looked up and generalize the associated type when it is not unknown: type(V,Env,T) :- ground(V), member(V:P,Env), generalize(P,T). generalize(P,T) :- nonvar(P), !, copy_term(P,T). generalize(T,T). Let's add two rules for tuples and addition, and change the syntax of let for clarity: type((A,B),Env,TA * TB) :- type(A,Env,TA), type(B,Env,TB). type(A+B,Env,number) :- type(A,Env,number), type(B,Env,number). type(let(X == XE, E),Env,ET) :- type(XE,Env,XT), type(E,[X:XT|Env],ET). Then, typing this: let(identity == lambda(v,v), let(increment == lambda(x,x+1), let(compose == lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))), (apply(apply(compose,identity),identity), apply(apply(compose,increment),increment))))) ... gives: (_1775 -> _1775) * (number -> number) You could also make use of meta attributes, ie. data stored inside variables, to control what happens during unification.

psygnisfive 9y ago

mm.. perhaps I'm just not familiar enough with prolog, but I don't think it's possible to extract out a set of Prolog-level metavariables and compute over them? This is what's necesary to turn something like `_G947 -> _G947` into `forall a. a -> a`. but probably I just don't know enough. cool if you can, tho!

tom_mellior 9y ago
That extraction is what the term_variables/2 predicate does that I use in my code. It gives you a list of all unbound variables in the given term. To simulate the quantification, I then just add that list in front of the term with the ^ operator (which has no semantics, it is just the traditional constructor for these things). So for `_G947 -> _G947` I get the variable list `[_G947]` and use it to represent the universally quantified term as `[_G947]^(_G947 -> _G947)`. If you want to display this with nicer variable names, just substitute names of your choice for the variables in the quantifier list.