Lambda the Ultimate

On first reading, I don't think the particular technique they describe would continue to work when the type language has nontrivial binding structure. (By "nontrivial", I mean "you need to do alpha-conversion when substituting type variables" -- system F, the polymorphic lambda calculus, is an example. ML-style polymorphism isn't, though.) To apply this to languages like System F you'd need higher-order unification, which is known to be undecidable. You could probably get a partial algorithm if you used this technique with lambda-Prolog or Twelf, though.

Personally, I think that when you are designing a type system for a language, as opposed to making a custom type system for a program analysis, you should specify the modes of the typechecking rules (a la bidirectional type checking). Among other things, this lets you declaratively specify where type annotations are and aren't needed.

I did almost the same thing (without the partial evaluation stuff) a couple of months ago for a advanced programming language course. I implemented an inferencer for the simple typed lambda calculus and the polymorphically typed lambda calculus. Both work briljantly and are very readable.

To apply this to languages like System F you'd need higher-order unification, which is known to be undecidable. You could probably get a partial algorithm

According to cardelli the accepted algorithm for polymorphic lambda calculus is indeed partial. This, however, is not a big problem since the terms seldom arise in pratice. See Cardelli - Types for a nce discussion of the system and the algorithm.

Here is the code for the type inference for the simple typed lambda calculus. Surprisingly it not only checks types, but infers them and can even calculate environments in which terms have certain types..

It can be called as follows:


infer( [[]], lambda( x:nat, x), X).


lambda terms are represented as the lambda( , ) atom and application by apply( , )

The first parameter given is the environment ( empty list of lists in this case.). Ascription is done using the ":" operator. The query should result in the answer (nat -> nat).

ps.
Hope i don't break any post etiquette with the length f this post.

:- op( 101, yfx,      : ),
   op( 400, yfx,      ->).

%%%%%%%%%%%%%%%%%
% Main F1 rules %
%%%%%%%%%%%%%%%%%

% basic types
basic( K ) :-
	member( K, [nat, bool] ).

% Env []
infer( [[]], valid).

% Env x
infer( [[X,A]|Rest], valid ) :-
	infer( Rest, A),
	not( member( [X,A], Rest)).

% Type Arrow
infer( Env, A -> B ) :-
	infer( Env, A),
	infer( Env, B).

% Type Const
infer( Env, K ) :-
	basic( K ),
	infer( Env, valid).

% Type Bool
infer( Env, bool) :-
	infer( Env, valid).

% Val True
infer( Env, true, bool) :-
	infer( Env, valid).

% Val False
infer( Env, false, bool) :-
	infer( Env, valid).

% Val x
infer( [[X,A]|Rest], X, A ) :-
	infer( [[X,A]|Rest], valid).

% Val Fun
infer( Env, lambda(X : A, M), A -> B ) :-
	infer( [[X,A]|Env], M, B).

% Val Appl
infer( Env, apply(M, N), B) :-
	basic( A ), 
	infer( Env, M, A -> B),
	infer( Env, N, A).

Link to a PDF.

I am not sure I get the problem here. What I have tended to do is implement type inference, and then check the types. So given an arbitrary expression and a type annotation, I would infer the type for the expression and then compare the type with the annotation. This gets it all done in one algorithm.

Using deferred constraint solving for HM seems unnecessary as you can resolve each constraint as you go along. This is what my bottom up type inference algorithm in pure Prolog does. You can see the algorithm for a simple lambda calculus here: https://github.com/keean/Clors/blob/master/example.cl This can infer types for open terms, from an empty environment, including polymorphic let bindings. It also deals with variable capture in a simple and elegant way.