%% 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)
10 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/
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
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.
*/
----
Hi great rreading your blog
Post a Comment