Lambda the Ultimate

(Note: this post assumes some familiarity with Kernel.)

Now that we've seen the resurrection of fexprs, I think it might be time to find out how to implement macro-like fexprs efficiently.

A previous post on this topic is Maybe with FEXPRs, which discusses expanding $cond into a chain of $if's (by Andres Navarro, who developed a Kernel implementation in C).

Let's take as an example the definition of $lambda in Kernel:

($define! $lambda
   ($vau (formals . body) env
      (wrap (eval (list* $vau formals #ignore body)
                  env))))

When the programmer writes ($lambda (x) (* x 2)), what we would like is for the code to be expanded to (wrap ($vau (x) #ignore (* x 2))) - analogous to how macros are expanded. (wrap is a Kernel primitive that induces evaluation of arguments, before calling an underlying combiner - a fexpr ($vau) with the body (* x 2) in this case.)

But given that a fexpr's body contains arbitrary Kernel code, this seems to require some form of "partial evaluation" or "abstract interpretation"... On the positive side, it seems intuitively doable - after all, the inputs to a fexpr are known, and if we have the programmer add some declaration that a fexpr has no side-effects, the compiler can go ahead and expand it at will. (Obviously, JIT recompilation is required in the general case - redefining a fexpr at runtime is possible just as redefining a function is.)

I'd be grateful for any ideas ideas and/or pointers!

[Edit: Ah, I guess I'll have to wade through Partial Evaluators for Scheme and Functional Programming Languages. PE'ing macro-like fexprs still seems much simpler than the general case: you only have to deal with terminating, side-effect-free computations, and moreover, the inputs are fully known - i.e. exactly the subset of computations that correspond to procedural macros. The case of non-terminating fexprs could be simply handled by aborting after a fixed number of reductions, emitting a warning, and leaving the code as-is for the usual runtime evaluation.]

Forgive the elementary nature of this question, but lacking the correct terminology, I'm having trouble getting started.

Consider the definition of a class A, together with a structural invariant (in the Guttag/Liskov/Meyer sense of that term). I'm trying to show that a certain class B is a "sort of" subtype of A, the sense that it obeys the Liskov/Wing substitution principle on all input for which the invariant holds, but not on input that causes the invariant to fail (in particular, methods of B will result in an error when the invariant does not hold, even if the same methods return normally for A objects).

Mind you, I'm not talking about the requirement that B preserve the same invariants as A (which is a basic component of the subtyping relationship). Rather, both have the same purported invariant, but B includes runtime invariant checks that result in failure as error, while the same methods in A might return normally, even though the encapsulated state might now violate the invariant. If the invariant truly holds in both A and B instances in all cases, then subtyping holds. It's only if we have an invariant failure (i.e. an implementation bug) that the difference shows up.

Is there an accepted term for this kind of "subtyping"? What is known about it?