[TYPES] Typechecking by partial evaluation

[Tim Sweeney]

Are any serious typecheckers based on a design like the following?

1. Implement a dynamically-typed runtime for language L' as a program P (written in language L), which takes a user program P' written in L', and runs P(P'), producing a type mismatch in any context where a value is used at the wrong type according to the type system of L'.

2. Given a partial evaluator for language L, partially evaluate P(P').

3. Reject the user program P' iff any runtime error productions remain in the partial-evaluated version of P(P').

I'm aware of the Futamura projection (http://en.wikipedia.org/wiki/Partial_evaluation), which applies steps 1-2 to give us a "compiler for free".  But haven't seen it carried to step 3, giving us a "typechecker for free".

This question arises during an attempt to implement a language with an advanced type system as a dynamically-typed runtime with zero compilation.  With this up and running, it intuitively feels like "there's a typechecker in there somewhere" which a partial evaluator could potentially extract.

For the curious, the language is based on concurrent constrant logic programming.  It performs, at runtime, the kinds of typeclass and overloading resolution that occur at compile-time in packages like GHC, using backtracking and narrowing to perform quantifier instantiation.

Tim Sweeney
Epic Games