<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div><div>On Jan 30, 2010, at 5:26 PM, Maurí cio CA wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: medium; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; ">Do you have some link to an example of such proof by induction of<br>type safety?</span></blockquote></div><br><div><font class="Apple-style-span" size="3"><span class="Apple-style-span" style="font-size: 12px; ">Not off-hand, but I did just find&nbsp;Atze Dijkstra's Essential Haskell, which covers the type system in depth, and it looks like a good bet for you. &nbsp;<span class="Apple-style-span" style="font-size: medium; "><a href="http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf">http://www.cs.uu.nl/groups/ST/Projects/ehc/ehc-book.pdf</a></span></span></font></div><div><br></div><div><font class="Apple-style-span" size="3"><span class="Apple-style-span" style="font-size: 12px; ">The principle is really easy. &nbsp;Since we deal with recursive structures so often, proof by induction boils down to proof by cases. &nbsp;You want to prove type safety for the base cases (the emitters), and prove that your combinators preserve type safety. &nbsp;But that's easy -- we get that for free since your combinators will be plain old Haskell functions. &nbsp;This would have been the induction step of the proof.&nbsp;</span></font></div><div><br></div><div>The principle is pretty simple. &nbsp;Consider the Haskell types:</div><div><br></div><div>&gt; data A = A deriving Show</div><div>&gt; data B = B deriving Show</div><div><br></div><div>&gt; data Pair = Pair { (A, B) }</div><div><br></div><div>And now let's say we want to turn a Pair into a Haskell function from A to B, as a string. &nbsp;I'm emitting Haskell since I don't know C. ;-)</div><div><br></div><div>&gt; emitPair :: &nbsp;Pair -&gt; String</div><div>&gt; emitPair (Pair (a,b)) = "pair " ++ show a ++ " = " ++ show b</div><div><br></div><div>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. &nbsp;To prove that emitPair meets the specification, you need to show that it emits the correct grammar. &nbsp;In fact, we can prove that emitPair emits type safe Haskell, in virtue of the fact that it is valid Haskell. &nbsp;Basically, to prove that your C emitters are type safe, you have to ensure that the code they emit is type safe.</div><div><br></div><div><div>You might want to create a sort of syntax tree data type to emit from. &nbsp;Or just create data types for each type of thing you want to emit. &nbsp; &nbsp;You can also create emitters that act on monadic values/actions. &nbsp;That might be a good option. &nbsp;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.</div><div><br></div><div>This idea can spiral out of control. &nbsp;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. &nbsp;Have fun!</div></div></div></body></html>