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

**/


9 comments:

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.

ertai said...

Hi,

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

[1]: http://www.haskell.org/pipermail/haskell-cafe/2010-November/085994.html
[2]: http://www.haskell.org/pipermail/haskell-cafe/2010-November/086016.html

Harry Stoteles said...
This comment has been removed by the author.
Harry Stoteles said...
This comment has been removed by the author.
Harry Stoteles 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/

Unknown said...
This comment has been removed by the author.
Farhad Mehta said...
This comment has been removed by the author.
Farhad Mehta said...

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

[2] http://www.haskell.org/pipermail/haskell-cafe/2010-November/086016.html

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.

Farhad Mehta

Farhad Mehta said...

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.
*/
----