%% 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
**/
Thursday, 31 January 2008
Type inference for The Simply Typed Lambda Calculus
Subscribe to:
Post Comments (Atom)
5 comments:
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.
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
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/
Post a Comment