How to go about a type checker in prolog?

prolog, typechecking

Solution

I intended what follows as a starting point. Here is my formalisation:

type(string).

means that string is an available type for a variable to be an instance of

signature(=, [X, X, nil]).

means that the infix operator = takes two arguments of same type and returns nothing.

is_instance(X, Y)

means that `X` is an instance of type `Y` To test things out, I created a list of "statements" contained in my variable `Input` of my `test/0` predicate. Then I recursively test out if things are well. You have to implement the third clause as a recursive call to find out if types are ok in expressions now.

What I did atm is that in my first main `check/2` clause, I handle `instance/2` terms, and in the following one, all the rest.

:- dynamic is_instance/2.

type(string).
type(int).

signature(=, [X, X, nil]).

test :-
    retractall(is_instance(_, _)),
    Input = [instance(s, string), instance(i, int), =(i, length(s))],
    check(Input, ReturnTypes),

check([], []).
check([instance(Variable, Type)|Terms], [nil|ReturnTypes]) :-
    !,
    ( is_instance(Variable, _) -> syntax_error('Variable already declared')
    ; \+ type(Type) -> syntax_error('Using a non-existing type'),
    ; Term =.. [is_instance, Variable, Type],
      assertz(Term)),
    check(Terms, ReturnTypes).

check([Term|Terms], [Type|ReturnTypes]) :-
    Term =.. [Name|Arguments],
    % Here we have to call ourselves with our list of arguments
    % and then check that everything is fine and then we'll unify Type
    % with the return value of Name.
    check(Terms, ReturnTypes).

I hope it'll help to get you started.

Problem

So I am new to prolog and I am suppose to implement a type checker. How exactly should I go about it? This would be an example: ``` String s; int i; i = s.length(); // OK (example given in the homework) ``` When I asked the professor how things will be input, it would look something like this: ``` instance(s, string). ``` Thats great, except if this is done, the unification for i is lost at the close of the query, so if I were to make a say, equals fact and call it like so, ``` equals(i, s, '.', 'length'). ``` how can i check what i is. So I am just having a hard time knowing where to start. Its a homework, so just want some advice, help on kind of understanding how to go about my first prolog project. Thanks in advance. EDIT: Assignment Write a Prolog program that can type check the method calls for a given Java program according to the JLS . The fact base can be any encoding of the methods defined in any non-trivial Java program you have written, plus, minimally, those listed below. In query mode, it must check potential matches; for example allowing "println(string)." You need not encode those JLS rules that you don't need. (One of the examples given is above.)

Original source