[TYPES] Typechecking by partial evaluation
Tim Sweeney
Tim.Sweeney at epicgames.com
Mon Aug 24 03:31:05 EDT 2009
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,
}
More information about the Types-list
mailing list