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

**/


5 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/