Hi, all, Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C? Using macro tricks or just good specifications? I know this is not absurd to a small extent. I've heard of proof tool certificated C code on the net (although I don't understand that theory), and I was also able to use what I learned from Haskell in a few C-like tasks. [*] So, I imagine if someone has done such kind of experiment seriously, like others have done with object-oriented programming (gobject etc.). Google told me nothing. Thanks, Maurício [*] This may actually be interesting. I had to use a proprietary script language mixing the worst of FORTRAN and C to drive an application, and I tried to use what I learned from Haskell by, say, prohibiting side effects out of some isolated code areas that got well specified input and gave well specified output -- even if the inside of the block itself was a huge mess. The result was actually fun to use, and after two years without looking at that code I was asked to adapt the application to be used inside another, which I could do in half a day! Maybe I should write a "Why functional programming matters - 2" on that :) It's easy to show FP is cool with abstract problems, but it's far more cool when we can show it can save even programmers with no CS theory background from huge headaches.
Maurício CA wrote:
Hi, all,
Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C? Using macro tricks or just good specifications?
I know there is some type level programming (not strictly functional) in CCAN: http://ccan.ozlabs.org/ Not sure if this is what you're after though. Erik -- ---------------------------------------------------------------------- Erik de Castro Lopo http://www.mega-nerd.com/
2010/1/29 Maurício CA:
Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C? Using macro tricks or just good specifications?
From the website: "SaC is an array programming language predominantly suited for application areas such as numerically intensive applications and signal
This is probably not what you're looking for, but it's related: Single-Assignment C ("Functional Array Programming for High-Performance Computing") http://www.sac-home.org/ processing. Its distinctive feature is that it combines high-level program specifications with runtime efficiency similar to that of hand-optimized low-level specifications. Key to the optimization process that facilitates these runtimes is the underlying functional model which also constitutes the basis for implicit parallelization. This makes SaC ideally suited for utilizing the full potential of modern CMP architectures such as multi-cores or the Cell processor." Regards, Sean
On Jan 29, 2010, at 9:11 AM, Maurí cio CA wrote:
Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C? Using macro tricks or just good specifications?
I know this is not absurd to a small extent. I've heard of proof tool certificated C code on the net (although I don't understand that theory), and I was also able to use what I learned from Haskell in a few C-like tasks. [*]
I would use a higher level language to emit valid C. Basically, use a strongly typed macro language. "All" you will have to prove is that your emitter produces type safe code, which you can do by induction and is straight forward. You can build up a small library of combinators for type safe units of C code. Haskell might be a good choice for writing your C pre-processor, but there are plenty of choices. Using something like ehaskell (or eruby) might be a good approach. http://hackage.haskell.org/package/ehaskell
Sorry if this looks weird, but do you know of experiences with functional programming, or "type programming", with C?
I would use a higher level language to emit valid C. Basically, use a strongly typed macro language. "All" you will have to prove is that your emitter produces type safe code, which you can do by induction and is straight forward.
This is interesting. I wasn't thinking at first about actual formal proofs, just some way to make small C posix-only programs easier to read an maintain by using a "big picture" functional look. But I would like to try that. Do you have some link to an example of such proof by induction of type safety? Thanks, Maurício
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!
participants (4)
-
Alexander Solla -
Erik de Castro Lopo -
Maurício CA -
Sean Leather