[Haskell-cafe] Type inference algorithm in Prolog and Haskell

[oleg at okmij.org]

Dan Doel wrote:

> Implementing type inference can be very easy in a logic language,
> because most of the work in a non-logic language is implementing
> unification:

> http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html

Correctly implementing type inference in Prolog is much more
complicated. The cited code is elegant, but it is not correct.

Here's the code without Unicode embellishments:

GNU Prolog 1.3.0
By Daniel Diaz
Copyright (C) 1999-2007 Daniel Diaz
| ?- [user].
compiling user for byte code...
:- op(150, xfx, --).
:- op(140, xfx, :).
:- op(100, xfy, ->).
:- op(100, yfx, $).

Gamma --    Term : Type   :- atom(Term), member(Term : Type, Gamma).
Gamma -- lam(A, B) : Alpha -> Beta :- [A : Alpha|Gamma] -- B : Beta.
Gamma --   A $ B : Beta   :- Gamma -- A : Alpha -> Beta, Gamma -- B : Alpha.

user compiled, 9 lines read - 1801 bytes written, 8746 ms

% We define a boolean and an integer constants -- only to make the examples
% smaller.

?- G0 = [i1:int, b1: bool], E = lam(f, lam(x, f $ (x $ i1))), G0 -- E : T.

  E = lam(f,lam(x,f$(x$i1)))
  G0 = [i1:int,b1:bool]
  T = (A->B)->(int->A)->B

% so far, so good.

?- G0 = [i1:int, b1: bool], E = lam(f, lam(x, f $ (x $ i1) $ (x $ b1))), 
     G0 -- E : T.
no

% Still good: we can't apply x both to a boolean and an integer.

?- G0 = [i1:int, b1: bool], 
     E = lam(f, lam(x, lam(x, f $ (x $ i1) $ (x $ b1)))), G0 -- E : T.

  E = lam(f,lam(x,lam(x,f$(x$i1)$(x$b1))))
  G0 = [i1:int,b1:bool]
  T = (A->B->C)->(bool->B)->(int->A)->C ? 

% What happened? How come we embedded an untypable term in a larger
% term, and it type-checked?
% Look at the type: why the first x has the type bool->B?
% Because two occurrences of x in the body of the term are
% different identifiers, one inner and one outer.
% The type checker does not understand lexical scoping!
% That is not Lambda-calculus!

% It gets worse:
| ?- E = lam(f, lam(x, (f $ (x $ lam(z,z))) $ (x $ (lam(u,lam(v,u)))))),
    [] -- E : T.

% lopes forever, has to be aborted.

?- E = lam(x, x $ x), [] -- E : T.
Illegal instruction: 4

Finally we've got a segmentation fault. I submit that a type-checker
that accepts ill-typed terms, loops and causes segmentation faults is
not correct.

The member() predicate is (one of the) culprits.  In a real
type-checker, if we find the binding x:t in Gamma and we fail to
type-check, we should not look for another binding in Gamma. We have
to fail. But that is not how member works: it selects one element from
the list; if it is not good, it selects another.

It is also tempting to use Prolog variables for lambda-bound
variables. That brings another can of worms: generally speaking, we
need disequality constraints.

Prolog sure makes some things easier, but some things quite more
complicated.

Implementing type inference for simply-typed lambda-calculus
in Haskell is not that complex:
	http://okmij.org/ftp/Computation/FLOLAC/TInfT.hs

However, we don't even have to do that. Haskell itself can do that for
us:
	http://okmij.org/ftp/tagless-final/course/TTF.hs

It boils out to three lines:

class Symantics repr where
    lam :: (repr a -> repr b) -> repr (a->b)
    app :: repr (a->b) -> repr a -> repr b

That is it: the type system of simply-typed lambda-calculus (which we
can read as the implication fragment of minimal logic). Two rules,
implication introduction and elimination, is all it takes. Now, when we
try to typecheck the problematic term

*TTF> lam (\x -> app x x)

<interactive>:1:17:
    Occurs check: cannot construct the infinite type: a = a -> b
      Expected type: repr a
      Inferred type: repr (a -> b)
    In the second argument of `app', namely `x'
    In the expression: app x x

we actually get a type error -- with a good error message -- rather
than a segmentation fault.