Remember the cliffhanger from Yannis’s previous talk? The problem with the program is that there could be conflicting names in the program already. So, what we need is constraints, like so:
Now, we may only generate for classes that do not have a conflicting getter yet. But how to type check this? We do not know anything about the existing class, we have no information about what X’s there could be, in terms of number and types of methods, fields etc.
This is a morpher that calls all methods of a class. How to know that this code is correct? Well, we know n comes from x, and we know that is takes in an into, as it is bound. To summarize: Morphing is special-purpose program generation. It is common in web frameworks and AOP approaches. There are close relatives with different levels of meta type-safety (Genoupe, CTR)
Why limit the host language? Why not come up with a more powerful language and proof that the generator will always generate valid code. However we need first-order logic for this. What exactly is first-order logic?
A family of languages with:
- true, false
- and, or, not
- universal quantifiers (forall, exists)
A specific instance of such a language could come with a number of functions and predicates, and this is exactly what we need.
So what type of propositions could we want to express for programs?
- HasType(y,t) <- think of reflection
- HasMethod(t,m) and HasReturn(m,t)
With this, we could express things like: (forall t: (exists m : HasMethod(t,m) and HasReturn(t,m)))
SafeGen is like morphing, it iterates over all the methods from the input class. An example: iterate over all methods such that each method has one argument that is public, and its return type has at least one method with an argument that implements java.io.Serializable. It is more powerful than morphing.
The idea behind type checking SafeGen programs is to describe everything in first order logic.
- Java well-formedness semantics: axioms
- Structure of generator/generated code: facts
- Type property to check: test
- Conjecture: (axioms (axioms ⋀ facts) → facts) → test
- Prove conjecture valid with a theorem prover (SPASS)
An example fact:
And this is a test (a very difficult way of expressing that the method names and types do not conflict)
But using a theorem prover, sometimes the proof generation does not terminate, in Yannis experience this happened in about 50% of the cases. So, instead of using FOL, why not use a dependently-typed language for the generator? With this, types can encode full proofs. (If you want to know more, have a look at Ur)
Yannis says that program generators are a new level of abstraction. If we know that the generated language is well-types, why care about the generated programs? Consider morphing: is it really program generation? Or is it just improved generics? Consider staging: is it really program generation? Or is it just helping the compiler specialize code?
As such it is just the next step in the story of procedural abstraction and type abstraction. The next step is structured abstraction: defining ‘things’ not necessarily generating a program based on a program’s structure. Both procedural and type abstraction got really big when they became safer, when we went from gotos to methods and from macros to generics. Structures are next!