On Jan 30, 2010, at 5:26 PM, Maurí cio CA wrote:

Do you have some link to an example of such proof by induction of

type safety?

The principle is really easy. Since we deal with recursive structures so often, proof by induction boils down to proof by cases. You want to prove type safety for the base cases (the emitters), and prove that your combinators preserve type safety. But that's easy -- we get that for free since your combinators will be plain old Haskell functions. This would have been the induction step of the proof.

The principle is pretty simple. Consider the Haskell types:

> data A = A deriving Show

> data B = B deriving Show

> data Pair = Pair { (A, B) }

And now let's say we want to turn a Pair into a Haskell function from A to B, as a string. I'm emitting Haskell since I don't know C. ;-)

> emitPair :: Pair -> String

> emitPair (Pair (a,b)) = "pair " ++ show a ++ " = " ++ show b

To use this, I would call emitPair from a Haskell source file, with a Pair as an argument, and it would define the function pair in the source file. To prove that emitPair meets the specification, you need to show that it emits the correct grammar. In fact, we can prove that emitPair emits type safe Haskell, in virtue of the fact that it is valid Haskell. Basically, to prove that your C emitters are type safe, you have to ensure that the code they emit is type safe.

You might want to create a sort of syntax tree data type to emit from. Or just create data types for each type of thing you want to emit. You can also create emitters that act on monadic values/actions. That might be a good option. You can hijack bind's semantics to make it concatenate your monadic action representation of a C fragment, and use do notation to write C code.

This idea can spiral out of control. The more granular you make the emitters/abstract syntax tree, the more your macro system becomes like a general purpose compiler for your own personal language. Have fun!