This one’s for the MIT crowd.
I will unfortunately not be in Boston over IAP, so I won’t be able to do a redux of the class I taught last year, Advanced Typeclasses in Haskell. However, since I will be in Boston for September, it might be a good time to do cluedump for SIPB this year. I love talking about Haskell, and so I could do another talk in a similar vein (maybe something that covers rank-2 types and existential quantification?) I’ve also been thinking that doing an architectural overview of Scripts would also be good.
Read more...
This part five of a six part introduction to c2hs. Today, we explain how to marshal data to and from C structures.
An important note. There is a difference between struct foo and foo; c2hs only considers the latter a type, so you may need to add some typedefs of the form typedef struct foo foo in order to get c2hs to recognize these structs.
Get. The Haskell FFI has no knowledge of C structs; Haskell’s idea of reading a member of a struct is to peek at some byte offset of a memory location, which you calculated manually. This is horrid, and hsc2hs has #peek to relieve you of this non-portable drudgery. c2hs has something even simpler: you can specify {#get StructName->struct_field #} and c2hs will replace this with a lambda that does the correct peek with the correct type: (\ptr -> do {peekByteOff ptr 12 ::IO CInt}) (in the IO monad!) Note the following gotchas:
Read more...
This is part four of a six part tutorial series on c2hs. Today we discuss the simple things in c2hs, namely the type, enum, pointer, import and context directives.
Prior art. All of the directives c2hs supports are tersely described in the “tutorial” page (which would perhaps be more accurately described as a “reference manual”, not tutorial.) There is also (paradoxically) a much more informal introduction for most of the directives in c2hs’s research paper.
Read more...
I’ve had a rather successful tenure with autogenerated documentation, both as a writer and a reader. So when Jacob Kaplan Moss’s articles on writing “great documentation” resurfaced on Reddit and had some harsh words about auto-generated documentation, I sat back a moment and thought about why autogenerated documentation leave developers with a bad taste in their mouths.
I interpreted Moss’s specific objections (besides asserting that they were “worthless” as the following:
Read more...
This is part three of a six part tutorial series on c2hs. Today, we take a step back from the nitty gritty details of FFI bindings and talk about more general design principles for your library.
On the one hand, writing an FFI binding can little more than churning out the glue code to let you write “C in Haskell,” the API of your library left at the whimsy of the original library author. On the other hand, you can aspire to make your interface indistinguishable from what someone might have written in pure Haskell, introducing modest innovation of your own to encode informally documented invariants from the C code into the type system.
Read more...
Last Tuesday, Eric Mertens gave the Galois tech talk Introducing Well-Founded Recursion. I have to admit, most of this went over my head the first time I heard it. Here are some notes that I ended up writing for myself as I stepped through the code again. I suggest reading the slides first to get a feel for the presentation. These notes are oriented towards a Haskell programmer who feels comfortable with the type system, but not Curry-Howard comfortable with the type system.
Read more...
This part two of a six part introduction to c2hs. Today, we discuss getting the damn thing to compile in the first place.
Reader prerequisites. You should know how to write, configure and build a vanilla Cabal file for pure Haskell. Fortunately, with cabal init, this is easier than ever. I’ll talk about how to setup a Cabal file for linking in C files, which is applicable to any sort of FFI writing (as it turns out, enabling c2hs is the trivial bit).
Read more...
Bjarne Stroustrup once boasted, “C++ is a multi-paradigm programming language that supports Object-Oriented and other useful styles of programming. If what you are looking for is something that forces you to do things in exactly one way, C++ isn’t it.” But as Taras Glek wryly notes, most of the static analysis and coding standards for C++ are mostly to make sure developers don’t use the other paradigms.
On Tuesday, Taras Glek presented Large-Scale Static Analysis at Mozilla. You can watch the video at Galois’s video stream. The guiding topic of the talk is pretty straightforward: how does Mozilla use static analysis to manage the millions of lines of code in C++ and JavaScript that it has? But there was another underlying topic: static analysis is not just for the formal-methods people and the PhDs; anyone can and should tap into the power afforded by static analysis.
Read more...
Attention conservation notice. The author reminisces about learning physics in high school, and claims that all too often, teaching was focused too much on concrete formulas, and not the unifying theory around them.
In elementary school, you may have learned D=RT (pronounced “dirt”), that is, distance is rate multiplied with time. This was mostly lies, but it was okay, because however tenuous the equation’s connection to the real world, teachers could use it to introduce the concept of algebraic manipulation, the idea that with just D=RT, you could also find out R if you knew D and T, and T if you knew D and R. Unless you were unusually bright, you didn’t know you were being lied to; you just learned to solve the word problems they’d give you.
Read more...