[Haskell-cafe] Re: C functional programming techniques?

[Alexander Solla]

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!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100131/b1bb9d18/attachment.html