algorithmic_typing.pl

% vim: ft=prolog


% Parser
% ------

parse(S, T) :- atom_chars(S, C), expr(T, C, []).

expr(E)                 --> ws, (statement(E) ; type(E)), ws.

lambda                  --> [λ] ; ['\\'].

arrow                   --> [→] ; [-, >].

ws1                     --> [' '], (ws1 ; []).
ws                      --> ws1 ; [].

lower(X)                --> [X], { char_type(X, lower) }.

statement(S)            --> abstraction(S)
                          ; if_term(S)
                          ; term(S).

term(A)                 --> application(A)
                          ; atom_term(A).

atom_term(P)            --> projection(P)
                          ; proj_base(P).

proj_base(P)            --> paren_term(P)
                          ; true_term(P)
                          ; false_term(P)
                          ; var_term(P)
                          ; record(P).

paren_term(S)           --> ['('], ws, statement(S), ws, [')'].

application(app(L, R))  --> atom_term(L), ws1, atom_term(R).

abstraction(λ(X, T, S)) --> abs_param(X), abs_type(T), abs_body(S).
abs_param(X)            --> lambda, ws, var_term(v(X)), ws.
abs_type(T)             --> [:], ws, type(T), ws.
abs_body(S)             --> [.], ws, statement(S).

var_term(v(X))          --> lower(X).

true_term(true)         --> [t,r,u,e].
false_term(false)       --> [f,a,l,s,e].
if_term(if(X, Y, Z))    --> [i,f], ws1, term(X), ws1, then_term(Y), else_term(Z).
then_term(Y)            --> [t,h,e,n], ws1, term(Y), ws1.
else_term(Z)            --> [e,l,s,e], ws1, term(Z).

proj_field(L)           --> label(C), { atom_chars(L, C) }.
label([C])              --> lower(C).
label([C|Cs])           --> lower(C), label(Cs).

projection(proj(B, F))  --> proj_base(B), ws, [.], ws, proj_field(F).

record(rec(M))          --> ['{'], ws, record_members(M), ws, ['}'].
record_members([M])     --> record_member(M).
record_members([M|Ms])  --> record_member(M), ws, [,], ws, record_members(Ms).
record_member([L, S])   --> proj_field(L), ws, [=], ws, statement(S).

type(T)                 --> func_type(T)
                          ; func_operand(T).

func_operand(O)         --> paren_type(O)
                          ; boolean_type(O)
                          ; top_type(O)
                          ; record_type(O).

paren_type(T)           --> ['('], ws, type(T), ws, [')'].

func_type(fn(A, B))     --> func_operand(A), ws, arrow, ws, func_operand(B).

boolean_type(bool)      --> ['B',o,o,l].

top_type(top)           --> ['T',o,p].

record_type(rcd(M))     --> ['{'], ws, rcd_members(M), ws, ['}'].
rcd_members([M])        --> rcd_member(M).
rcd_members([M|Ms])     --> rcd_member(M), ws, [,], ws, rcd_members(Ms).
rcd_member([L, T])      --> proj_field(L), ws, [:], ws, type(T).


% Typing
% ------

map_lookup([[X, T] | _], X, T) :- !.
map_lookup([_ | M], X, T) :- map_lookup(M, X, T).

typeof(X, T) :- typeof([], X, T).

% Lambda calculus

typeof(G, v(X), T) :-
    map_lookup(G, X, T).
typeof(G, λ(X, T, B), fn(T, S)) :-
    typeof([[X, T] | G], B, S).
typeof(G, app(L, R), S2) :-
    typeof(G, L, fn(S1, S2)),
    typeof(G, R, T),
    subtype(T, S1).

% Records

typeof(_, rec([]), rcd([])).
typeof(G, rec([[L, V] | Rec]), rcd([[L, T] | Rcd])) :-
    typeof(G, V, T),
    typeof(G, rec(Rec), rcd(Rcd)).
typeof(G, proj(R, L), T) :-
    typeof(G, R, rcd(Rcd)),
    map_lookup(Rcd, L, T).

% Booleans

typeof(_, true, bool).
typeof(_, false, bool).

typeof(G, if(X, Y, Z), J) :-
    typeof(G, X, bool),
    typeof(G, Y, T2),
    typeof(G, Z, T3),
    join(T2, T3, J).


% Subtyping
% ---------

subtype(T, T) :- !.
subtype(_, top).

subtype(fn(S1, S2), fn(T1, T2)) :-
    subtype(T1, S1),
    subtype(S2, T2).

subtype(rcd(_), rcd([])).
subtype(rcd(R1), rcd([[L, T] | R2])) :-
    map_lookup(R1, L, S),
    subtype(S, T),
    subtype(rcd(R1), rcd(R2)).


% Joins
% -----

map_pluck([], _, nil, []).
map_pluck([[L, T] | R], L, T, R) :- !.
map_pluck([[K, S] | R], L, T, [[K, S] | R_]) :-
    map_pluck(R, L, T, R_).

map_no_member(R, L) :- map_pluck(R, L, S, _), S = nil.

join(S, S, S) :- !.

join(fn(S1, S2), fn(T1, T2), fn(M1, J2)) :-
    meet(S1, T1, M1),
    join(S2, T2, J2),
    !.

join(rcd([]), rcd(_), rcd([])) :- !.

join(rcd([[L, S] | R1]), rcd(R2), rcd([[L, K] | J])) :-
    map_lookup(R2, L, T),
    join(S, T, K),
    join(rcd(R1), rcd(R2), rcd(J)),
    !.

join(rcd([[L, _] | R1]), rcd(R2), rcd(J)) :-
    map_no_member(R2, L),
    join(rcd(R1), rcd(R2), rcd(J)),
    !.

join(_, _, top).


% Meets
% -----

meet(S, S, S) :- !.

meet(top, T, T).
meet(S, top, S).

meet(fn(S1, S2), fn(T1, T2), fn(J1, M2)) :-
    join(S1, T1, J1),
    meet(S2, T2, M2).

meet(rcd([]), rcd(R2), rcd(R2)).

meet(rcd([[L, S] | R1]), rcd(R2), rcd([[L, N] | M])) :-
    map_pluck(R2, L, T, R2_),
    meet(S, T, N),
    meet(rcd(R1), rcd(R2_), rcd(M)).

meet(S, nil, S).