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

ertai said...

Hi,

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