osa1

Type checking with Prolog

June 13, 2013 - Tagged as: en, prolog, types.

There is a deep relation between a type inference system and a logic programming system. I don’t fully understand this relation. This question I asked at StackOverflow a few months ago gives some tips, but doesn’t explain much.

I could finally spare some time and play with a type checker implementation in Prolog. What I had in mind before starting writing this code was that having a unification mechanism at hand should make type checking easier.

Indeed that is the case, as you’ll see shortly. Type inference is harder, and I also explain the reason and how could it be done.

I will not formally define the type system here, but I think it can be seen as a simple Damas-Hindley-Milner style type system.

This implementation basically embeds type definitions in Prolog. This is what makes this implementation simple. You can always implement a fully-featured type system in Prolog just like you can do it in any other language. What I’m trying to show here that it’s very simple to do when there is a way to implement types as rules in Prolog.

Here’s knowledge base of types:

nat(o).
nat(s(N)) :- nat(N).

bool(true).
bool(false).

type(A, nat) :- nat(A), !.
type(A, bool) :- bool(A), !.
type(id, arrow(A, A)) :- !.
type(add, arrow(nat, arrow(nat, nat))) :- !.
type(not, arrow(bool, bool)) :- !.
type(const, arrow(A, arrow(_, A))).

Implementing type definitions as rules in a Prolog system is what makes this implementation simple. Here id is a function with type forall a. a -> a, add is nat -> nat, not is bool -> bool, and const is forall a b. a -> b -> a.

Type checking of function applications is also simple:

type(app(F, P), R) :-
    type(F, arrow(A, R)),
    type(P, A).

And we’re done. This much code is enough for type checking polymorphic functions. Here are some examples:

?- type(app(id, false), T).
T = bool.

?- type(app(id, o), T).
T = nat.

?- type(app(add, o), T).
T = arrow(nat, nat).

?- type(app(app(add, o), s(o)), T).
T = nat.

?- type(app(app(add, o), false), T).
false.

?- type(app(app(const, false), o), T).
T = bool.

?- type(app(app(const, false), true), T).
T = bool.

One major limitation of this implementation is that there is no way to implement monomorphic functions. To do this, we should somehow have two different kinds of Prolog variables, one for polymorphic variables and one for monomorphic ones.

Since there’s no way to directly express this in Prolog, I had to extend this code with a typing environment. In the implementation above, if parameter of a function is an atom and not a variable, then it’s looked in a global environment.

type(app(F, P), R) :-
    type(F, arrow(A, B)),
    var(A), % polymorphic parameter
    type(P, A),
    R = B,
    !.

type(app(F, P), R) :-
    type(F, arrow(A, B)),
    atom(A), % monomorphic parameter
    get_type(types, A, TypeA),
    % type already exists in environment
    !,
    type(P, TypeA),
    type_in_env(B, R),
    !.

type(app(F, P), R) :-
    type(F, arrow(A, B)),
    atom(A), % monomorphic parameter
    % type doesn't exist in environment
    type(P, TypeP),
    add_type(types, A, TypeP),
    type_in_env(B, R),
    !.

First rule is for polymorphic parameters, only difference from the first code is var(A), which ensures the parameter type is a variable.

Second rule does a similar check, but this time to ensure the parameter is an atom and not a variable. After that, type of this parameter is looked from an environment and checked against it. The third rule is when a type is not found in the environment. In that case, a new type is added to the environment.

Note that first cut is required in second rule. Because otherwise, when a type checking fails, third rule would be executed and a new type would be added to the environment.

Here are environment operations:

init_state(Name) :-
    empty_assoc(A),
    nb_setval(Name, A).

add_type(SName, TermName, Type) :-
    nb_getval(SName, State),
    put_assoc(TermName, State, Type, NewState),
    nb_setval(SName, NewState).

get_type(SName, TermName, Type) :-
    nb_getval(SName, State),
    get_assoc(TermName, State, Type).

Environment operations get a environment name to keep the state local. ie. you can be sure your state is local if name of the state is not used somewhere else :-)

This helper is used to get type of a term when term is an atom, and it’s type is available in environment. Otherwise it returns the term itself.

type_in_env(T, T1) :- get_type(types, T, T1).
type_in_env(T, T).

An example monomorphic function rule:

type(mono_id, arrow(mono_id__a, mono_id__a)) :- !.

It should be guaranteed by the programmer that mono_id__a atom is only used for mono_id function.

Here are some examples for checking monomorphic functions(others work as before):

?- init_state(types).
true.

?- type(app(mono_id, o), T).
T = nat.

?- type(app(mono_id, s(o)), T).
T = nat.

?- type(app(mono_id, false), T).
false.

?- init_state(types).
true.

?- type(app(mono_id, false), T).
T = bool.

?- type(app(mono_id, o), T).
false.

This code should demonstrate how easy it’s to implement a type checker when there’s a way to express typing rules as Prolog rules. We had type checker for polymorphic and monomorphic functions in 57 lines of Prolog.

For type inference, we need to generate new rules in runtime. I’m looking for ways to do this. assert/1 and dynamic/1 predicates make this possible, but I still couldn’t find a way to generate fresh Prolog variables(like gensym, but for variables). I’ll update this post later.

(Show comments)