[TYPES] Typechecking by partial evaluation

[Marco Devillers]

Although I cannot totally follow this discussion, I don't think it'll
work. I don't fully understand what a CCLP language would be, I think
of your proposition as: can we (partially) type-check programs with a
'prolog-like' interpreter?

> * 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.

Yeah, that'll work - but what is the real difference with an elaborate
interpreter where partial evaluation isn't constrained to, say, just
some form of beta-reduction, but also uses some heavy optimization
like lifting function over/into other functions? Wouldn't that be
roughly exactly as strong as two-directional information passing?
I.e., if you can pass values upward/downward 'flexible' enough, you
get the same power as a simple type inferencer. (Guess I am stating
the obvious here for you all.)

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

What would the rules be used in such a partial-evaluator, and are you
sure it would be a strong as a 'heavy optimizer' where more elaborate
rules might be given?

> * 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 am not informed enough to follow, but I don't have the feeling that
any typed program with partial evaluation would 'really' be able to
infer more information than what could be inferred by partial
evaluation by a strong optimizer. I would like to see some examples
elaborated. But yeah, this is where its getting interesting.

On Mon, Aug 24, 2009 at 9:31 AM, Tim Sweeney<Tim.Sweeney at epicgames.com> wrote:

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

So did I :), great slides on your last talk Tim.