Automatic type inference via partial evaluation

Automatic type inference via partial evaluation. Aaron Tomb, Cormac Flanagan. PPDP’05.

Type checking and type inference are fundamentally similar problems. However, the algorithms for performing the two operations, on the same type system, often differ significantly. The type checker is typically a straightforward encoding of the original type rules. For many systems, type inference is performed using a two-phase, constraint-based algorithm.We present an approach that, given the original type rules written as clauses in a logic programming language, automatically generates an efficient, two-phase, constraint-based type inference algorithm. Our approach works by partially evaluating the type checking rules with respect to the target program to yield a set of constraints suitable for input to an external constraint solver. This approach avoids the need to manually develop and verify a separate type inference algorithm, and is ideal for experimentation with and rapid prototyping of novel type systems.

Also somewhat relevant to the discussions here about type checking as abstract interpretation.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

On first reading, I don't thi

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 (

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

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.

Inference First

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