Arity-aware type Inference
-----------------------------
more or less standard definitions, haven't needed changing from the
non-arity aware case:
member(Key, cons(Head, Tail), Val) :-
dif(Key,Head),
member(Key, Tail, Val).
member(Key, cons(def(Key, Val), Tail), just(Val)).
member(Key, nil, nothing).
append(cons(H, T1), L, cons(H, T2)) :-
append(T1, L, T2).
append(nil, L, L).
unifyall(cons(T, Tail), T) :-
unifyall(Tail, T).
unifyall(nil, T).
unifyeach(cons(Tapp, Tail), Tdef, Cxt) :-
duplicate_term(Tdef, pair(C1, Tapp)),
unifyeach(Tail, Tdef, Csub),
append(Csub, C1, Cxt).
unifyeach(nil, T, nil).
split(X, cons(def(Y, T), Tail1), Tail2, cons(def(Y, T), Tail3)) :-
dif(X, Y),
split(X, Tail1, Tail2, Tail3).
split(X, cons(def(X, T), Tail1), cons(T, Tail2), Tail3 ) :-
split(X, Tail1, Tail2, Tail3).
split(X, nil, nil, nil).
nat(zero).
nat(succ(X)) :-
nat(X).
bool(true).
bool(false).
New arity-aware type inference algorithm:
expr(P, var(X), cons(def(X, Type), nil), Type).
expr(P, nat(X1), nil, nat) :-
nat(X).
expr(P, bool(X), nil, bool) :-
bool(X).
expr(P, pair(X, Y), C3, prod(A, B)) :-
expr(pair, X, C1, A),
expr(pair, Y, C2, B),
append(C1, C2, C3).
expr(app, app(Fun, Arg), Cxt, B) :-
expr(app, Fun, C1, arrow(M, A, B)),
expr(app, Arg, C2, A),
append(C1, C2, Cxt).
expr(P, app(Fun, Arg), Cxt, B) :-
dif(P, app),
expr(app, Fun, C1, arrow(y, A, B)),
expr(app, Arg, C2, A),
append(C1, C2, Cxt).
expr(P, lam(Var, lam(VV, BB)), Cxt, arrow(n, A, B)) :-
expr(lam, lam(VV, BB), C1, B),
split(Var, C1, Def, Cxt),
unifyall(Def, A).
expr(P, lam(Var, Body), Cxt, arrow(y, A, B)) :-
dif(Body, lam(X, Y)),
expr(lam, Body, C1, B),
split(Var, C1, Def, Cxt),
unifyall(Def, A).
expr(P, let(Var, Body, Rhs), Cxt, T2) :-
expr(let, Body, C1, T1),
expr(let, Rhs, C2, T2),
split(Var, C2, Def, C3),
unifyeach(Def, pair(C1, T1), C4),
append(C3, C4, Cxt).
Examples:
let test = \f . \x . \y . f x y in test
Which is represented by:
let(test, lam(f, lam(x, lam(y, app(app(var(f), var(x)), var(y))))),
var(test))
The query is:
:- expr(root,
let(test, lam(f, lam(x, lam(y, app(app(var(f), var(x)), var(y))))),
var(test)),
Cxt, Typ).
The Result (omitting proof):
yes(Cxt7 = nil, Typ1 = arrow(n, arrow(M2, T6, arrow(y, T7, B6)),
arrow(n, T6, arrow(y, T7, B6)))).
Which, translating into infix arrows is:
test :: ('t6 -'m1-> 't7 -y-> 'b6) -n-> 't6 -n-> 't7 -y-> 'b6
Which looks correct to me. The inference determine a lambda is a call-site
if it does not directly contain a nested lambda.
\x . let f = \y . \x . (x, (y, z)) in f
is represented as:
lam(x, let(f, lam(y, lam(z, pair(var(x), pair(var(y), var(z))))),
var(f)))
and the typing query is written:
:- expr(root, lam(x, let(f, lam(y, lam(z, pair(var(x), pair(var(y),
var(z))))), var(f))), C, T).
and gives the result:
yes(C1 = nil, T8 = arrow(y, T9, arrow(n, T10, arrow(y, T11, prod(T9,
prod(T10, T11)))))).
which rewritten looks like:
't9 -y-> 't10 -n-> 't11 -y-> ('t9, ('t10, 't11))
The determination for an application is made depending on if is is directly
nested inside another application so:
let f = a b c in f c
is represented by:
let(f, app(app(var(a), var(b)), var(c)), app(var(f), var(d)))
and the query is therefore:
:- expr(root, let(f, app(app(var(a), var(b)), var(c)), app(var(f),
var(d))), C, T).
and we get the result:
yes(C2 = cons(def(d, Type2), cons(def(a, arrow(M3, Type3, arrow(y,
Type4, arrow(y, Type2, T23)))), cons(def(b, Type3), cons(def(c, Type4),
nil)))), T12 = T23).
looking at the type of "a":
a : arrow(M3, Type3, arrow(y, Type4, arrow(y, Type2, T23))
which rewritten is:
a : 'type3 -'m-> 'type4 -y-> 'type2 -y-> 't23
which again looks correct.
Unification of these types is normal unification. So, that's type inference
for arity-aware types sorted... Okay what have I forgotten? :-)
Keean.
On 3 April 2015 at 03:12, Matt Oliveri <[email protected]> wrote:
> On Thu, Apr 2, 2015 at 5:22 PM, Jonathan S. Shapiro <[email protected]>
> wrote:
> > On Thu, Apr 2, 2015 at 4:15 AM, Matt Oliveri <[email protected]> wrote:
> >> We don't want intuitionistic type-theory's way, which is to use
> >> dependent types. Dependent types for an imperative language is cutting
> >> edge stuff, and Shap decided not to try to do that yet.
> >
> > shap is still very unhappy about that outcome. I would say rather that
> shap
> > has decided to defer consideration of dependent types, except to make
> sure
> > that we don't do something stupid in our surface syntax to preclude them.
>
> OK. Thanks for the correction.
>
> > However: shap still harbors an unhappy suspicion that we *need* dependent
> > types. Given this, I definitely think we should consider the
> implications of
> > our designs in the context of the appropriate dependent type theories.
> >
> > Or at least that's what shap thought when I spoke to him last...
>
> You talk like this it seems whenever I tell someone about what "Shap"
> said. I'm talking about you, of course. Your signature just says
> "shap". Would you like me to refer to you some other way? Or should I
> never try to report what you've said?
> _______________________________________________
> bitc-dev mailing list
> [email protected]
> http://www.coyotos.org/mailman/listinfo/bitc-dev
>
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
