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

Alexander Solla ajs at 2piix.com
Sun Jan 31 03:22:30 EST 2010

```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
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
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