## Thursday, 31 January 2008

### Type inference for The Simply Typed Lambda Calculus

`%% Type inference for The Simply Typed Lambda Calculus:- op(150, xfx, ⊢).:- op(140, xfx, :).:- op(100, xfy, ->).:- op(100, yfx, \$).Γ ⊢    Term : Type          :- atom(Term), member(Term : Type, Γ).Γ ⊢ λ(A, B) : Alpha -> Beta :- [A : Alpha|Γ] ⊢ B : Beta.Γ ⊢   A \$ B : Beta          :- Γ ⊢ A : Alpha -> Beta, Γ ⊢ B : Alpha./** Examples:% Typing fix?- Γ ⊢ y \$ f : Y, Γ ⊢ f \$ (y \$ f) : Y.Γ = [y: (Y->Y)->Y, f:Y->Y|_G330]% Typing the Y combinator?- Γ ⊢ λ(f, (λ(f,f \$ f)) \$ (λ(g,f \$ (g \$ g)))) : Y.Y = (_G309 -> _G309) -> _G309 % Typing flip id?- Id = λ(i, i), Flip = λ(f, λ(y, λ(x, f \$ x \$ y))),   Γ ⊢ Flip \$ Id : T.T = _G395 -> (_G395 -> _G411) -> _G411**/`

Sean Braithwaite said...

Im really enjoying your posts. Please keep writting them. Its nice to more advanced programming topics engaged with, even if i don't fully understand them.

np said...

Hi,

There is a thread on the Haskell-Cafe which mentioned this post [1], in particular Oleg answer [2].

Jan Burse said...
This comment has been removed by the author.
Jan Burse said...
This comment has been removed by the author.
Jan Burse said...

I don't like the idea that the code does not make use of an occurs check in the unification.

I guess you could give a type to self application like (F F), but we might want to avoid this.

http://stackoverflow.com/questions/3702855/typing-the-y-combinator/

This comment has been removed by the author.
This comment has been removed by the author.

I would like to suggest an improvement to this solution to address shortcomings raised in [2]:

Improvement:

Replace the call to member/2 with isInTypeEnv/2 defined as follows:

/*
* A version of member/2 with the occurs check enabled (to avoid infinite types),
* that stops searching once a mapping with the same variable name is found.
*/
isInTypeEnv(Var:Type, [EVar:EType|_]) :- Var=EVar,!,unify_with_occurs_check(Type,EType).
isInTypeEnv(Var:Type, [_|T]) :- isInTypeEnv(Var:Type,T).
/*
* Note: The (red) cut (!) in the above definition is important. Without it, updates to the
* type environment Γ would not result in "overwriting", leading to erroneous
* type inference and checking.
* /

With this modification, it seems that the issues raised in [2] do not occur any more.

An improvement to my last message: isInTypeEnv/2 could be defined in a better, more declarative way without the cut (what was I thinking! 🙄) as follows:

----
/*
* A version of member/2 with the occurs check enabled (to avoid infinite types),
* that stops searching once a mapping with the same variable name is found.
*/
isInTypeEnv(Var:Type, [EVar:EType|_]) :- Var = EVar, unify_with_occurs_check(Type,EType).
isInTypeEnv(Var:Type, [EVar:_|T]) :- Var \= EVar, isInTypeEnv(Var:Type,T).
/*
* Note: Checking that Var\=EVar before searching further in the above definition is important.
* Without it, updates to the type environment Γ would not result in "overwriting", leading to erroneous
* type inference and checking.
*/
----