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-lam...
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.