Lambda the Ultimate

I think it depends mostly on how powerful the language is and how much control you want. For example, I've been doing some metaprogramming in Coq recently, which is possible because Coq's type system is powerful enough to express proofs of type-correctness.

For example, let's say 'AST' is our AST datatype and 'eval' is an interpreter. We could give 'eval' the following type:

Definition eval : AST -> option {t : Type & t}

This says we take in an AST and give out an option/maybe value, ie. "None" or "Some x", where "x" is a dependent pair containing a type and a value of that type. The 1st and 2nd elements of a dependent pair can be extracted using "projT1" and "projT2", which lets me write the following dependent functions:

(* Extract the type, defaulting to unit for "None" *)
Definition extractType (x : option {t : Type & t}) : Type
        := match x with
               | None    => unit
               | Some x' => projT2 x'
           end.

(* Extract the value, defaulting to unit for "None" *)
Definition extractValue (x : option {t : Type & t}) : extractType x
        := match x with
               | None => tt
               | Some x' => projT1 x'
           end.

I can compose these quite easily:

Definition runExtract (x : AST) : extractType (eval x)
        := extractValue (eval x).

runExtract is perfectly valid anywhere in my program, as long as its return type unifies with the type required at that point (ie. it type-checks). This requires that 'extractType (eval x)' can be computed statically, in other words the type of the AST's value must be static, but its value can still be dynamic; for example if we compute the type using lazy evaluation, the value will be left unevaluated.

I'm not sure how much of this is lost as we reduce the power of the language; the formulation above makes heavy use of dependent types, for example. Note that this is actually a common pattern for implementing DSLs in dependently-typed languages, although I've not seen it used to self-host (ie. where AST can represent any Coq term). Doing so seems to be undecidable. I've been working around by limiting recursion depth, so Coq-with-depth-N+1 can evaluate ASTs for Coq-with-depth-N.

In the case of C, the language has basically no existing support for type-safe code rewriting. Adding it would require the following:
1) A representation of ASTs, along with a library of functions for creating them, manipulating them, traversing them, etc.
2) A theorem-prover with a model of C's type system and the AST representation.
3) A compiler for turning ASTs into machine code.

Given the above, we can generate programs in AST form by using the AST library. We can then use the theorem prover to show that our AST program has the C type we want. We can them compile it with the AST compiler, load it into memory and jump to it (this may require some indirection, depending on the machine architecture and OS; eg. x86 Linux doesn't allow executing data).

The thing is, C's type system is incredibly weak, so there's not much point going to all this effort just to maintain some flimsy semblance of safety. It's much easier to just dump code into RAM and jump to it, safety be damned.

If a language has a powerful type system, like Haskell for example, then the safety guarantees may be worth the effort of dumping ASTs through a compiler.

If the language has a really powerful type system, like Coq, we can push those safety guarantees right back into the AST-generating functions, to guarantee that ill-typed ASTs can never be generated in the first place.

I don't know why you'd want to mutate the AST at run time. I'm not aware of any language that allows this, statically typed or not (except maybe Perl 6, I'm not sure). You *can* however do Lisp style macros in a statically typed language. Check out Scala for example. Also check out MetaOCaml for a language extension that lets you generate new code at run-time.

Your question is weirdly interesting, so I want to know your train of thought making you think of this. Can you articulate your motive prompting the idea? (It's okay if it's hazy and hypothetical; a lot of useful reasoning starts that way before careful sorting.)

If the program entities (is there a better word?)

Term "entity" is sufficiently vague you can use it to refer to anything. So it's good as an all-inclusive bucket catching everything.

may be manipulated at runtime, is it still possible to type-check the program at compile-time?

That sounds like, "If I dynamically alter at runtime what I statically checked at compile time, is the static check still valid?" Only by luck, I would think, since you ought to be able to violate any invariant established at compile time, making the static check no longer true.

Let me ask a more practical question: How would ANSI C, as an example, would have to be extended in order to provide direct read and write access to the abstract syntax tree at runtime while not losing its compile-time type-checking feature.

In your scenario, does altering the AST affect the running code, immediately or later? When does new code corresponding to the new AST get generated and run? It's a desire to write the AST at runtime that puzzles me. Is it for exploratory programming? Would generating new source to run later be enough for experiments?

I plan to rewrite C only to change when things happen, so async calls can occur, structured as yielding to a trampoline at call time. But the idea is to alter only when something happens, which C doesn't really care about, as opposed to what happens, which ought to stay the same. I only want to end up with another encoding of the same AST, so the goal is unchanged invariants when timing doesn't matter.

My transformation is narrow and simple, while yours sounds arbitrarily complex, if you allow any runtime rewrite. All I have to do is find all calls to functions that yield, then heap allocate a refcounted parameter block for formal parameters and return to the trampoline dispatcher to make the actual downcall, with the rest of the function turned into a separate function called as the continuation (also provided with the downcall info).

[A function that yields is one that blocks, makes an async call, takes too long, or calls another function that yields. The resulting "yield propagation" is similar to const propagation, so you could infer most of it from global analysis, provided the base cases are clearly declared for blocking, long-running, or async-calling.]

If you tell folks what you want to happen, they can make better suggestions. So far it sounds like you want to destabilize something already painfully fragile, in the case of C. You must have a payoff justifying some risk.

You seem to be alluding to some kind of provisions (via library support or native language constructs) to allow for arbitrary self-modifying code.

I can't make any judgment a priori (nor either way) without more info on the use cases you have in mind, but I'm rather intrigued by your, say, "insisting" to attempt it at the AST level in particular.

Of course, self-modifying code is pretty common these days, if only in the case of managed environments (Java, .NET, etc), but it's usually done in a "disciplined" way (well, if I dare say) via runtime support and reflection capabilities over runtime "entities" that have been designed to support it in a (relatively) type safe way, precisely - e.g., app domains, assemblies, modules, reified runtime types, etc, in .NET (cf. System.Reflection, ...)

But also, and perharps more importantly, when that's done, it's AFAIK only allowed within the controlled bounds of one *major* assumption - not random at all - and kept in check by the same language runtime :

that it will only be "okay" of *augmenting* the computation facilities of the running program (i.e., compiling *new* types and functions/methods bodies), as opposed to tampering with/unloading the pre-compiled modules that were loaded at application start (not allowed)**.

In short, my perplexity/curiosity joins quite naturally that of McCusker's, as I concur.

'HTH.

**I personally interpret it in such a managed environment runtime, for an analogy with the Church-Turing thesis, as :

once a new theorem (~ new runtime type) is derived/learned (~ loaded) thanks to a pre-existing theory (~ pre-loaded modules), you can't quite afford to change it or to "unlearn" it, or at least not before you're willing to discard it along with everything else (~ application shutdown) that allowed to introduce it, and to put it to work to possibly build others, etc (if only for keeping consistency)

.