[TYPES] Typechecking by partial evaluation

[Tim Sweeney]

Oleg,

Thanks for the insight and reference.  I've followed your writings for many years and found them inspiring.

I became painfully familiar with the limitations of partial-evaluation-as-typechecking in a previous attempt to define a functional programming language this way.  But when applied to a Concurrent Constraint Logic Programming language, this scheme appears to become unusually powerful and compact:

* Since constraints can propagate values in both directions within a CCLP language runtime, partially-evaluated constraints can propagate partial value information (values, types, approximations, or similar) in both directions.

* Since backtracking is built into the constraint-logic language, the partial-evaluator can use native backtracking to verify potential execution paths.

* Since a CCLP can instantiate the equivalent of existential and universal quantifiers in certain contexts, we gain type-like expressiveness with these constructs, using only the runtime's underlying value operations.

I have yet to carry out the full experiment, but the early results do look promising.  It seems plausible that this approach can achieve a level of typechecking expressiveness comparable with e.g. GHC's support for Haskell typeclasses, given a runtime that implements all of those features dynamically, and a relatively small amount of additional logic for reasoning about types and approximations.

Tim

________________________________________
From: oleg at okmij.org [oleg at okmij.org]
Sent: Monday, August 24, 2009 12:32 AM
To: Tim Sweeney; types-list at lists.seas.upenn.edu
Subject: [TYPES] Typechecking by partial evaluation

> 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,
}