[TYPES] Typechecking by partial evaluation

[oleg@okmij.org]

> 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 am afraid partial evaluation -- which is said to be a glorified
constant propagation -- is not powerful enough. Let's consider the
program 
	let n = read in
	if n then n+1 else n
or, fun n -> if n then n+1 else n

The variable n is marked dynamic, the test and the both branches of
the if-expression are dynamic. The partial evaluator can't do anything
but residualize. The type error (assuming HM type system) will not be
noticed. We need a static analysis that notices that the test of the
if expression makes sense only if n is a boolean. The static analysis
would then _propagate_ this _positive information_ down the
if-branches, and run into a contradiction. It seems that we need at
least positive supercompilation. Positive and the general
supercompilation are very well explained in

@InProceedings{	sorensen-unifying,
  author	= {S{\o}rensen, Morten Heine B. and Gl{\"u}ck, Robert and Jones, Neil D.},
  title		= {Towards Unifying Deforestation, Supercompilation, 
                   Partial Evaluation, and Generalized Partial Computation},
  pages		= {485--500},
  crossref	= "esop1994",
  url		= "ftp://ftp.diku.dk/diku/semantics/papers/D-190.ps.gz",
}