[TYPES] Typechecking by partial evaluation

[voigt@tcs.inf.tu-dresden.de]

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list
> ]
>
> 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').

The following paper:

http://doi.acm.org/10.1145/1480881.1480889

proposes a design that is similar in spirit.

There clearly are differences. The issue there is not type errors, but
more properties like "head of empty list". And instead of a partial
evaluator, GHC's built-in optimization strategies are used.

But the similarity lies in the combination of introducing explicit error
calls for undesired behavior (step 1), aggressive optimization (step 2),
and naive syntactic checks for remaining error calls (step 3).

Ciao,
Janis.