% A simple Hindley-style type inference algorithm written in Prolog
% Alan Mycroft, January 2007.

% Expressions:
% Expr ::= icon(int) | var(string) | lam(string, Expr) | app(Expr, Expr)

% Type Expressions:
% Type ::= tint | tarrow(Type,Type)

% Type Environments:  list of (string,Type) pairs

% In 'lookup' the use of cut (!) ensures that we only find the most
% recent (i.e. non-scope-shadowed) version of a variable when the
% names of lambda-bound variables are not distinct.
lookup(X, [(X,T)|TEnv], T) :- !.
lookup(X, [(_,_)|TEnv], T) :-  lookup(X, TEnv, T).

infer(var(X), TEnv, T) :- lookup(X,TEnv,T).
infer(icon(_), TEnv, tint).
infer(lam(X,E), TEnv, arrow(T1,T2)) :- infer(E, [(X,T1)|TEnv], T2).
infer(app(F,E), TEnv, T2) :- infer(F, TEnv, arrow(T1,T2)),
                             infer(E, TEnv, T1).

% a test function:

typeofScombinator(T) :-
  infer(lam(f,lam(g,lam(x,
          app(app(var(f),var(x)), app(var(g),var(x)))))),
        [],
        T).

% Note the following bug due to Prolog not doing
% proper(occurs-check) unification:

bug(T) :-
  infer(lam(x, app(var(x),var(x))), [], T).