Re: Adding Identities to Peval

[Andy Wingo <wingo@pobox.com>]

On Thu 16 Feb 2012 14:18, Noah Lavine <noah.b.lavine@gmail.com> writes:

>>  (let ((x (random)))
>>    (eq? x x))
>
> (let* ((x (random))
>        (y (list x))
>        (z (car y))
>   (eq? x z))

This one should reduce to the same thing, but currently doesn't because
(list x) is not considered a "constant expression" because `let' is a
"constructor" (quotes to indicate the language of peval).  If we can
propagate it (probably true in this case, given that it has only one
use), then the expression folds as before:

  (let* ((x (random))
         (z (car (list x))))
    (eq? x z))
  => 
  (let ((x-129 (random))) 
    (eq? x-129 x-129)))

So I don't think that for this purpose (identity) we need any more
mechanism

> In order to type-check, you need to be able to associate extra
> information with a value (its type) even in cases where you don't know
> the value.

For this purpose, have you considered creating a functional database of
facts?  Then you can add facts when you see conditionals, for example,
and you get different facts in the different branches.

  (if test consequent alternate)
  ;; assuming the test doesn't fold
  => (make-if (for-test test current-facts)
              (for-tail consequent (add-fact test #t current-facts))
              (for-tail consequent (add-fact test #f current-facts)))

You can also join the facts accumulated by a conditional branch with the
current facts if you detect that one of the branches leads to a nonlocal
exit, as in

  (define (foo x)
    (if (not (and (struct? x) (eq? (struct-vtable x) <foo>)))
        (error ...))
    ;; here at this point, we have the fact: x is a struct, and its
    ;; vtable is <foo>
    ...)

This is related to range analysis.  But, it's also something that's
easier to do with an explicit notion of control flow (i.e. a CPS IR).

Regards,

Andy
-- 
http://wingolog.org/