[tom_mellior]

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]

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]

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]

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.