[psygnisfive]

Ahh, well! That's a trickier problem! You need a bidirectional system that has unification for metavariables, and then some system for handling unsolved metavars. But to do that requires a more complicated set up. The goal of the post was to introduce the core ideas and show that it's relatively simple to do decent chunks of this stuff. :)

[junke]

Type inference can be easy too, here is a 5mn Prolog thing:

    type(X,_,number) :- number(X).

    type(V,Env,T) :-
        ground(V),
        member(V:T,Env).

    type(<(X,Y),Env,bool) :-
        type(X,Env,number),
        type(Y,Env,number).

    type(or(A,B),Env,bool) :-
        type(A,Env,bool),
        type(B,Env,bool).

    type(lambda(X,E),Env,XT -> ET) :-
        type(E,[X:XT|Env],ET).

    type(apply(F,E),Env,T) :-
        type(E,Env,ET),
        type(F,Env,ET->T).

    type(let(X,XE,E),Env,ET) :-
        type(XE,Env,XT),
        type(E,[X:XT|Env],ET).

For example:

    ?- type(lambda(f,lambda(g,lambda(x,apply(f,apply(g,x))))),[],T).
    T = ((_232 -> _226) -> (_225 -> _232) -> _225 -> _226)

[psygnisfive]

Indeed! Tho this is only half the problem, because `T` there includes metavariables, so it's not a type but rather a schema at the meta-level for types. What we'd like is something like `forall a b c. (b -> c) -> (a -> b) -> a -> c` so that composition can be used at arbitrary choices of the types. So like, while we can use this composition function at any particular place we need composition, we can't define `compose` to have this type because the first use site will force the metavars to have a particular value and then we get a nasty global monomorphism. We need to explicitly have metavariables in the language itself, rather than at the metalevel of doing the synthesis/checking.

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

[junke]

Yes, details are tricky. Thanks for the detailed comment.