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?
Not off-hand, but I did just find Atze Dijkstra's Essential Haskell,
which covers the type system in depth, and it looks like a good bet
for you. http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf
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!_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
