Haskell Embedded: Functional Programming and Embedded Systems http://haskellembedded.github.io//atom.xml 2016-09-23T00:00:00Z Introducing Ion http://haskellembedded.github.io//posts/2016-09-23-introducing-ion.html 2016-09-23T00:00:00Z 2016-09-23T00:00:00Z Posted on September 23, 2016 by Chris Hodapp
Tags: haskell, ivory

Really Short Version

Ion is a Haskell EDSL that I wrote for concurrent, realtime, embedded programming, targeting the Ivory EDSL. I finally released it to hackage. It’s still rather experimental.

Background: Atom & Ivory

Last year, I wrote a few posts on Atom. Remember Atom? If not, those posts might give some useful background.

At some work at my former job, I was already using Atom in conjunction with Ivory, but those two libraries really weren’t made for interfacing with each other. Atom predates Ivory, but they both model certain features of the C language, and as a result have many near-identical-but-incompatible constructs. For some boring details on this, see the section on this hackery.

Sometime after this, I decided to re-implement Atom’s functionality in a more Ivory-friendly way. I looked around in the Atom source code first with the aim of adding an Ivory backend to it, however, I quickly gave up on this as the internals were a bit too dense for me to follow.

This post is badly-overdue, and for that I apologize. For more information, track me (hodapp) down in #haskell-embedded or Ion’s GitHub.


Here, then, is where I started writing the Ion library from scratch. The name ‘Ion’ is a pun that’s a reference to ‘Atom’ and meaning loosely that while Atom is more standalone, Ion exists bonded to another library, Ivory. (I should probably move away from chemistry puns and leave that up to things like Rust and Redox.)

For the most part, I liked the way that Atom worked, and I wanted Ion to behave very similarly. Particularly, I liked the way that I could modularize a specification with the Atom monad, the way that specs could ‘inherit’ schedule parameters, the single run-time report giving the entire schedule of the system, and the checks that Atom’s compiler did to ensure that specifications were sensible.

Ion started here, but diverged somewhat later on. I didn’t manage to match all the features that are in Atom (and I note some of this in Ion’s documentation), and I started down some other paths.

What is Ion?

Ion, in brief, is a Haskell EDSL for concurrent, realtime, embedded programming. It targets the Ivory EDSL and is coupled closely with it.

I made Ion to cover two main cases:

  • Scheduling tasks (“tasks” loosely just meaning “little bits of restricted Ivory code”) that needed to execute on very strict timing.
  • Using continuating-passing style to compose together asychronous tasks (particularly those that call around with callbacks).

I sort of gloss over the “why?” of the first part because it’s almost all of the same reasons of why Atom exists. I try to answer the “why?” of the second part, and to some extent the “how?”, below.

Async & CPS

In the application that was using Ion, I started integrating in some support for network communication via a SIM800 GSM modem. This involved many operations of transmitting a command over a UART, waiting for a reply sometime in the future which contained the result of that command - perhaps an HTTP payload or something.

Or, maybe it didn’t - maybe it just contained some minor error, and the command should be retried.

Or, maybe it was a fatal error, and the only thing left to do was try to close down the connections, power off the modem, and power off the UART.

Or, maybe the reply was just total garbage from the UART.

Or, maybe something left the modem in a weird state, and it sent no reply at all because it’s still waiting for us to do something.

The world of rigid, deterministic timing didn’t really have a place for this sort of uncertainly-timed, non-deterministic, divergent behavior (someone’s probably codified this into a theorem or something). Actually, I had tried my best to make some similar and simpler procedures work in Atom. I made specifications which ran with the same rigid timing regardless of when operations actually finished, and to make this reliable, I set that timing to be very slow, and had parts of the specification disabled if earlier steps failed. It worked, but operations took up far more time than needed, and handling anything more divergent than if this fails, don’t run that would become very messy.

This also is a bit tricky to handle in C in any context without threads or coroutines. It almost always will involve callbacks, interrupts, or events - some scope starts an asynchronous operation (e.g. triggering an ADC measurement), and the result comes in the form of an interrupt handler or callback later being called. That callback/interrupt handler/event handler will have to run in a separate scope - which means that any state that needs to make it ‘across’ to that handler cannot reside on the stack. It must be stored in some other form, and recovered at the handler. (I found out at some point that this has been described already: it is called stack ripping, and it comes with event-driven programming.)

That’s annoying as-is, but in my case, I didn’t even have a heap from which to dynamically allocate, so the only remaining option was static memory.

As a side note, Ivory does provide a nice coroutines implementation, but I ran into two issues with them: They put every variable (whether ‘live’ across a suspend/yield or not) into static memory, and they were not composable. An appendix section gives some more details on this.

I wanted coroutines I could parametrize over other coroutines (higher-order coroutines?), which seemed to require something like a coroutine whose ‘resume’ continuation and ‘exit’ continuation both were reified rather than implicit. I also wanted it to be in a form that I could interface it with C APIs that wanted function pointers for callbacks or “normal” functions for interrupts.

I do not have a reference on this, but from memory, one of Oleg Kiselyov’s papers defined a coroutine as something like, “two continuations calling each other.” After thinking on this a bit, I realized that coroutines weren’t really the appropriate abstraction; I needed something more general, perhaps like a continuation, because ultimately what I was dealing with was continuation-passing style, and indeed CPS can express other patterns such as exceptions. (After reading extensively about Control.Monad.Cont and trying to discern whether I could use Cont, ContT, MonadCont, or callCC to achieve this, I decided that I had even less of an idea than when I started. I was leaning towards “no,” but I still have no idea.)

In the end, I ignored coroutines completely. I made a couple basic abstractions and some plumbing to make them practically usable, and this worked well for me. The CPS section gives some further examples on this.


The examples here are all rather contrived. All of the “real” work that I did with Ion was proprietary code that I can’t share, and even if I could, it wouldn’t build to an actual embedded target, except in the context of the much larger Shake build it was in and the entire associated toolchain.

However, I’ve tried to create some representative examples to a hypothetical C API. See Example.hs for these examples in a more buildable form (at least as far as the Haskell part goes).


First, let’s tell Ivory about some (nonexistent) C calls in something.h, with corresponding C prototypes indicated above for those who have no idea how to grok Ivory declarations:

-- void foo(int16_t)
foo :: Def ('[Sint16] :-> ())
foo = importProc "foo" "something.h"

-- void bar(int32_t)
bar :: Def ('[Sint32] :-> ())
bar = importProc "bar" "something.h"

-- uint16_t get_value(int32_t)
get_value :: Def ('[Uint8] :-> Uint16)
get_value = importProc "get_value" "something.h"

-- bool get_flag(void)
get_flag :: Def ('[] :-> IBool)
get_flag = importProc "get_flag" "something.h"

Here’s a top-level spec. As with Atom, period defines what division of a base rate all of its contents inherit - hence, variousPhases (which I define later) runs at 1/100th of the base rate, unless that’s overridden.

simpleSchedule :: Ion ()
simpleSchedule = ion "schedule" $ do
  period 100 $ do

  cond ((>? 10) <$> call get_value) $ do
    ivoryEff $ comment "get_value() > 10"
    cond (call get_flag) $ do
      ivoryEff $ comment "get_value() > 10 && get_flag()"

The entire cond block is there to illustrate that parts of a spec can be made conditional. The argument to cond isn’t exactly a boolean, but rather, is an Ivory effect which returns a boolean. One denotes the Ivory effects to weave into all of this with ivoryEff, and in this case, the code does the very boring effect of inserting a C comment with comment.

Here is variousPhases:

variousPhases :: Ion ()
variousPhases = do
    phase 1 $ ivoryEff $ do
      comment "period 100, phase 1"
      call_ foo
    phase 10 $ ion "optional_tag" $ ivoryEff $ do
      comment "period 100, phase 10"
      call_ bar
    disable $ phase 20 $ ivoryEff $ do
      comment "shouldn't even appear in code"
      call_ foo
      call_ bar
    delay 50 $ do
      p <- getSched
      ivoryEff $ do
        comment "Should be phase 100 + 50"
        comment ("Reported sched: " ++ show p)
      delay 10 $ ion "moreDelay" $ do
        p <- getSched
        ivoryEff $ do
          comment "Should be phase 100 + 50 + 10"
          comment ("Reported sched: " ++ show p)
      phase 1 $ do
        ivoryEff $ comment "Should override to phase 1"
    period 1000 $ do
      ivoryEff $ comment "Should override all other period"

This is full of phase, which behaves more like exactPhase from Atom, specifying that its contents should execute at some specific offset of the current period. I don’t yet have support for the exact semantics of Atom’s phase, which means something more like, “schedule it then, at the earliest”.

delay has no exact analogue in Atom, but it simply specifies that something executes at some relative phase past the phase that was inherited. That is, if you nested a series of delay 1, they’d all proceed one tick apart, starting at what phase they inherited.

If we run all this through Ion and Ivory with ionCompile ivoryOpts "simpleSchedule" simpleSchedule then the below C code results:

// module simpleSchedule Source:

#include "simpleSchedule.h"
uint8_t counter_schedule_0 = (uint8_t) 1U;
uint8_t counter_optional_tag_1 = (uint8_t) 10U;
uint8_t counter_schedule_2 = (uint8_t) 50U;
uint8_t counter_moreDelay_3 = (uint8_t) 60U;
uint8_t counter_schedule_4 = (uint8_t) 1U;
uint16_t counter_schedule_5 = (uint16_t) 0U;
uint8_t counter_schedule_6 = (uint8_t) 0U;
uint8_t counter_schedule_7 = (uint8_t) 0U;
void simpleSchedule(void)
    /* Auto-generated schedule entry procedure from Ion & Ivory */
    /* Path: schedule */
    if ((bool) ((uint8_t) 0U == counter_schedule_0)) {
        counter_schedule_0 = (uint8_t) 99U;
    } else {
        counter_schedule_0 = (uint8_t) (counter_schedule_0 - (uint8_t) 1U);
    /* Path: schedule.optional_tag */
    if ((bool) ((uint8_t) 0U == counter_optional_tag_1)) {
        counter_optional_tag_1 = (uint8_t) 99U;
    } else {
        counter_optional_tag_1 = (uint8_t) (counter_optional_tag_1 - (uint8_t) 1U);
    /* Path: schedule */
    if ((bool) ((uint8_t) 0U == counter_schedule_2)) {
        counter_schedule_2 = (uint8_t) 99U;
    } else {
        counter_schedule_2 = (uint8_t) (counter_schedule_2 - (uint8_t) 1U);
    /* Path: schedule.moreDelay */
    if ((bool) ((uint8_t) 0U == counter_moreDelay_3)) {
        counter_moreDelay_3 = (uint8_t) 99U;
    } else {
        counter_moreDelay_3 = (uint8_t) (counter_moreDelay_3 - (uint8_t) 1U);
    /* Path: schedule */
    if ((bool) ((uint8_t) 0U == counter_schedule_4)) {
        counter_schedule_4 = (uint8_t) 99U;
    } else {
        counter_schedule_4 = (uint8_t) (counter_schedule_4 - (uint8_t) 1U);
    /* Path: schedule */
    if ((bool) ((uint16_t) 0U == counter_schedule_5)) {
        counter_schedule_5 = (uint16_t) 999U;
    } else {
        counter_schedule_5 = (uint16_t) (counter_schedule_5 - (uint16_t) 1U);
    /* Path: schedule */
    if ((bool) ((uint8_t) 0U == counter_schedule_6)) {
        counter_schedule_6 = (uint8_t) 0U;
    } else {
        counter_schedule_6 = (uint8_t) (counter_schedule_6 - (uint8_t) 1U);
    /* Path: schedule */
    if ((bool) ((uint8_t) 0U == counter_schedule_7)) {
        counter_schedule_7 = (uint8_t) 0U;
    } else {
        counter_schedule_7 = (uint8_t) (counter_schedule_7 - (uint8_t) 1U);
void ion_schedule_0(void)
    /* Auto-generated schedule procedure from Ion & Ivory */
    /* Path: schedule */
    /* Phase: 1 */
    /* Period: 100 */
    /* Action has no conditions */
    /* period 100, phase 1 */
void ion_optional_tag_1(void)
    /* Path: schedule.optional_tag */
    /* Phase: 10 */
    /* Period: 100 */
    /* Action has no conditions */
    /* period 100, phase 10 */
void ion_schedule_2(void)
    /* Path: schedule */
    /* Phase: 50 */
    /* Period: 100 */
    /* Action has no conditions */
    /* Should be phase 100 + 50 */
    /* Reported sched: Schedule {schedId = 0, schedName = "schedule", schedPath = ["schedule"], schedPhase = 50, schedPeriod = 100, schedAction = [], schedCond = []} */
void ion_moreDelay_3(void)
    /* Path: schedule.moreDelay */
    /* Phase: 60 */
    /* Period: 100 */
    /* Action has no conditions */
    /* Should be phase 100 + 50 + 10 */
    /* Reported sched: Schedule {schedId = 0, schedName = "moreDelay", schedPath = ["schedule","moreDelay"], schedPhase = 60, schedPeriod = 100, schedAction = [], schedCond = []} */
void ion_schedule_4(void)
    /* Path: schedule */
    /* Phase: 1 */
    /* Period: 100 */
    /* Action has no conditions */
    /* Should override to phase 1 */
void ion_schedule_5(void)
    /* Path: schedule */
    /* Phase: 0 */
    /* Period: 1000 */
    /* Action has no conditions */
    /* Should override all other period */
void ion_schedule_6(void)
    /* Path: schedule */
    /* Phase: 0 */
    /* Period: 1 */
    /* Action has 1 conditions: */
    uint16_t n_r0 = get_value();
    if ((bool) (n_r0 > (uint16_t) 10U)) {
        /* get_value() > 10 */
void ion_schedule_7(void)
    /* Path: schedule */
    /* Phase: 0 */
    /* Period: 1 */
    /* Action has 2 conditions: */
    bool n_r0 = get_flag();
    uint16_t n_r1 = get_value();
    if ((bool) (n_r0 && (bool) (n_r1 > (uint16_t) 10U))) {
        /* get_value() > 10 && get_flag() */

and this header:

// module simpleSchedule Header:

#include "ivory.h"
extern uint8_t counter_schedule_0;
extern uint8_t counter_optional_tag_1;
extern uint8_t counter_schedule_2;
extern uint8_t counter_moreDelay_3;
extern uint8_t counter_schedule_4;
extern uint16_t counter_schedule_5;
extern uint8_t counter_schedule_6;
extern uint8_t counter_schedule_7;
void simpleSchedule(void);
void ion_schedule_0(void);
void ion_optional_tag_1(void);
void ion_schedule_2(void);
void ion_moreDelay_3(void);
void ion_schedule_4(void);
void ion_schedule_5(void);
void ion_schedule_6(void);
void ion_schedule_7(void);

simpleSchedule is the most important of this: This is the main scheduling function (“schedule entry procedure”) that must be called at the base rate through a timer, an interrupt, or something of the sort for anything to work right. Often this must be set up outside of Ivory because Ivory really isn’t interested in whatever C/ASM black magic the timer requires - go do that, hide it, and don’t let Ivory know about it. Also, the name of that function is what we supplied to ionCompile.

It has also produced several variables, all of the counter_ ones, which are used for establishing the correct periods and phases. Take a look in simpleSchedule and the pattern should be clear (as well as near-identical to how Atom does it, since I basically copied its method): Each Ivory effect in a particular period/phase context turns into a branch, a function, and a counter variable. The counter variable starts at the respective phase, and each branch is responsible for resetting it to the respective period, decrementing the counter, and calling the function that contains the Ivory effects. Note also that counter_schedule_5 uses a uint16_t - it corresponds to the period 1000 block, so a larger counter variable is needed to fit that range. Note also in ion_schedule_7 that nesting conditions with cond leads to all of them applying (i.e. logical AND).

Read through the code in some more detail, and it should be clear how specifications map and flatten out to generated C code. The names given in ion are for the most part just for documentation purposes; Ion is perfectly content to generate unique C identifiers without help. Note that each point has a sort of “path” that led to it, and that path determines how it is scheduled.


Here’s a shorter example that incorporates Ion’s resettable timers (note the use of mdo so we may define the timer first; this will need {-# LANGUAGE RecursiveDo #-}):

exampleTimer :: Ion (Def ('[] ':-> ()))
exampleTimer = ion "timer" $ mdo

  -- Timer is initialized with a Uint16; procedure called at
  -- expiration is fixed at compile-time:
  timer1 <- period 1 $ timer (Proxy :: Proxy Uint16) expire

  -- Initialization procedure:
  init <- newProc $ body $ do
    -- Trigger the timer for 1000 ticks:
    startTimer timer1 1000
  expire <- newProc $ body $ do
    call_ printf "Timer expired!\r\n"

  return init

This makes use of the Ion monad to return the entry procedure, which is required to start the timer counting in the first place. Also, due to some limitations, the timer’s behavior upon expiration is fixed at compile-time, though its countdown time is not (hence the 1000 we pass to startTimer). Rather than calling some external procedure when the timer expires (as we did in the prior section), we use newProc to define a procedure right there, and Ion takes care of giving it a name and having Ivory include it. To simplify things, we put the timer inside of period 1 so it counts at the base rate - but if, for instance, the base rate were 1 millisecond, we might sensibly put the timer inside period 1000 so that its countdowns are all in seconds.

The resultant C source is below:

// module timer Source:

#include "timer.h"
uint16_t timer_0 = (uint16_t) 0U;
uint8_t counter_decr_0 = (uint8_t) 0U;
void timer_1(void)
    timer_0 = (uint16_t) 1000U;
void timer_2(void)
    printf("Timer expired!\r\n");
void timer(void)
    /* Path: timer.timer_0.decr */
    if ((bool) ((uint8_t) 0U == counter_decr_0)) {
        counter_decr_0 = (uint8_t) 0U;
    } else {
        counter_decr_0 = (uint8_t) (counter_decr_0 - (uint8_t) 1U);
void ion_decr_0(void)
    /* Path: timer.timer_0.decr */
    /* Phase: 0 */
    /* Period: 1 */
    /* Action has no conditions */
    uint16_t n_deref0 = timer_0;
    if ((bool) ((uint16_t) 0U == n_deref0)) { } else {
        uint16_t n_cse1 = (uint16_t) (n_deref0 - (uint16_t) 1U);
        timer_0 = n_cse1;
        if ((bool) (n_cse1 > (uint16_t) 0U)) { } else {

and the header:

// module timer Header:

#include "ivory.h"
extern uint16_t timer_0;
extern uint8_t counter_decr_0;
void timer_1(void);
void timer_2(void);
void timer(void);
void ion_decr_0(void);

This should look similar to the last section, but with the addition now of timer_0. Our procedure with newProc was also turned into the C function timer_2.


The next example might be a bit trickier to understand, but I hope that it both explains both this functionality and what I mean when I talk about ‘composing’ things.

I’ll start with a smaller piece rather than a larger one this time. Suppose we’re dealing with some kind of async API with uint16_t transmit_async(uint16_t opcode, void (*callback)(uint16_t)) - it transmits opcode, it returns some kind of immediate success/error code as a uint16_t (perhaps an error indicates a failure to even transmit), and when the opcode returns a result, then it calls callback with some payload.

Given the right machinery, this actually composes pretty easily with continuation-passing style. Consider the below, which connects this function to two other callbacks - a different “error” callback (perhaps we produce our own error code of another format), and a “success” callback - and returns for us an initialization procedure:

exampleSend :: Word16 -- ^ Payload value (or something like that)
               -> Def ('[Uint32] ':-> ()) -- ^ Error callback
               -> Def ('[Uint16] ':-> ()) -- ^ Success callback
               -> Ion (Def ('[] ':-> ()))
exampleSend payload err succ = mdo

  let transmit_async :: Def ('[Uint16, ProcPtr ('[Uint16] :-> ())] :-> Uint32)
      transmit_async = importProc "transmit_async" "foo.h"

  write <- newProc $ body $ do
    comment $ "Transmit value: " ++ show payload
    -- Tell transmit_async to transmit this, and call us back at 'recv'
    -- (which we define after):
    errCode <- call transmit_async (fromIntegral payload) $ procPtr recv
    -- Check for a nonzero error code:
    ifte_ (errCode /=? 0)
      (call_ err errCode)
      $ return ()

  recv <- newProc $ \value -> body $ do
    -- Say that hypothetically we should have received the same value
    -- back, so check this first:
    ifte_ (value /=? fromIntegral payload)
      -- If a mismatch, then call the error handler with some code:
      (call_ err 0x12345678)
      -- Otherwise, call the success handler:
      $ call_ succ value

  return write

Remember that timer module we used in the last section, and how it was parametrized over a callback to be called upon expiration? We could probably easily rig this into exampleSend so that a failure to receive a reply within N milliseconds would trigger the error callback. (I’m not going to do that - this is just an example of how one can combine callbacks.)

Slight aside: You might notice the use of mdo again. This is because otherwise the definitions would have to go in reverse order of their calls. Consider the following:

foo = do
  call1 <- newProc $ body $ call_ call2
  call2 <- newProc $ body $ call_ call3
  call3 <- newProc $ body $ call_ call4
  call4 <- newProc $ body $ call_ call5
  callN <- newProc $ body $ retVoid

call1 calls call2, which calls call3, which calls call4, and so on. They’re in the order in which they’d be called. However, this is invalid code, because the definition of call1 relies on a definition that comes later. If we actually reordered these to be valid, then definitions would be backwards from the order in which they’re called. The simplest solution I found was just to use mdo.

Back to exampleSend: Now that it’s defined in this format, we can build it up into larger things. Consider the below definition which invokes it three times:

exampleChain = mdo
  let error :: Def ('[Uint32] :-> ())
      error = importProc "assert_error" "something.h"

  init <- exampleSend 0x1234 error =<<
          adapt_0_1 =<< exampleSend 0x2345 error =<<
          adapt_0_1 =<< exampleSend 0x3456 error =<<
          adapt_0_1 =<< exampleSend 0x4567 error success

  success <- newProc $ \_ -> body $ do
    call_ printf "All calls succeeded!\r\n"

  return init

This chains together 4 calls to exampleSend to create a procedure that will try to send opcodes 0x1234, 0x2345, 0x3456, and 0x4567. If any step fails, assert_error is called (though we could just as easily parametrize exampleChain over a separate error callback). If every step succeeds, it calls the internal procedure success (of course, again, we could parametrize over this callback too). It returns the entry procedure which starts this entire process.

I haven’t explained adapt_0_1 yet, but it’s just a piece of plumbing to stick together mismatched C functions. The success callback takes a single Uint16, but we for whatever reason don’t need it, so adapt_0_1 throws away that value and just calls the entry procedure of exampleSend (which takes no arguments).

This produces the below C code:

// module exampleChain Source:

#include "exampleChain.h"
void exampleChain_0(void)
    /* Transmit value: 17767 */
    uint32_t n_r0 = transmit_async((uint16_t) 17767U, exampleChain_1);
    if ((bool) ((uint32_t) 0U != n_r0)) {
void exampleChain_1(uint16_t n_var0)
    if ((bool) (n_var0 != (uint16_t) 17767U)) {
        assert_error((uint32_t) 305419896U);
    } else {
void exampleChain_2(uint16_t n_var0)
void exampleChain_3(void)
    /* Transmit value: 13398 */
    uint32_t n_r0 = transmit_async((uint16_t) 13398U, exampleChain_4);
void exampleChain_4(uint16_t n_var0)
    if ((bool) (n_var0 != (uint16_t) 13398U)) {
        assert_error((uint32_t) 305419896U);
    } else {
void exampleChain_5(uint16_t n_var0)
void exampleChain_6(void)
    /* Transmit value: 9029 */
    uint32_t n_r0 = transmit_async((uint16_t) 9029U, exampleChain_7);
void exampleChain_7(uint16_t n_var0)
    if ((bool) (n_var0 != (uint16_t) 9029U)) {
        assert_error((uint32_t) 305419896U);
    } else {
void exampleChain_8(uint16_t n_var0)
void exampleChain_9(void)
    /* Transmit value: 4660 */
    uint32_t n_r0 = transmit_async((uint16_t) 4660U, exampleChain_10);
void exampleChain_10(uint16_t n_var0)
    if ((bool) (n_var0 != (uint16_t) 4660U)) {
        assert_error((uint32_t) 305419896U);
    } else {
void exampleChain_11(uint16_t n_var0)
    printf("All calls succeeded!\r\n");
void exampleChain(void)

and the below C header:

// module exampleChain Header:

#include "ivory.h"
void exampleChain_0(void);
void exampleChain_1(uint16_t n_var0);
void exampleChain_2(uint16_t n_var0);
void exampleChain_3(void);
void exampleChain_4(uint16_t n_var0);
void exampleChain_5(uint16_t n_var0);
void exampleChain_6(void);
void exampleChain_7(uint16_t n_var0);
void exampleChain_8(uint16_t n_var0);
void exampleChain_9(void);
void exampleChain_10(uint16_t n_var0);
void exampleChain_11(uint16_t n_var0);
void exampleChain(void);

Note that this is all done with no static variables. It has no need to store a continuation, call stack, or anything of the sort. Of course, it’s not magic. You still need to use static variables for state that lives across calls, and external APIs have to store their callbacks someplace.

Note one particular limitation here (the same one as with timer): When you parametrize an Ion over procedures, those procedures are fixed at C compile-time. Ivory may now allow some means of storing function pointers in such a manner that you could work past this limitation, but if memory serves me, when I wrote this Ivory had no way to store a function pointer in static memory. I accepted this limitation because it made for much better-defined behavior, as I saw it.

This is fairly representative of the way that I used this functionality, just a bit simpler. When I used it for network communications, it took a form more akin to exception handling, as it would run through a sequence of steps for which the proper way to handle a failure differed depending on step. In that instance, I had an entire chain of shutdown steps (e.g. close TCP connection; drop modem connection; turn off modem; turn off UART; and disable power source), and callbacks would jump to different parts of it.


Ion helped me immensely with generating large amounts of C plumbing whose behavior was very easy to reason about. It also cut both ways, as it made it trivial to very quickly occupy a lot of RAM, generate a lot of unnecessary code, and produce huge binaries.

Much of the aforementioned plumbing was to bundle together the boilerplate that Ivory requires - things like incl for every single function that actually needs to be a C function by way of an Ivory procedure. In Haskell-world, one doesn’t normally think of having to explicitly declare each function, but Ivory inherits this C limitation. When Ion has to generate a lot of Ivory procedures and variables (particularly when I’m using it to parametrize these definitions over something), it has to accumulate all of this somehow and get it to Ivory’s compiler.

I tried to fix the bugs in Ion that pertained to correctness, but it still has a lot of room for improvement when it comes to efficiency and comprehensibility of the generated code for scheduling, and part of that is because it errs on the side of paranoia.

Appendix 1: Atom & Ivory hackery

Atom and Ivory both generate C code, and to that end, both express many of the same features of the C programming language - very central things like expressions, variables, conditionals, and the C type system. However, they have different purposes in mind (otherwise, why would I be using both?) and were never really meant to interface with each other. The way they model those features then is identical or similar, but incompatible.

However, I needed the two libraries to generate C code in the same build, to be able to refer to Atom variables from Ivory (and vice versa), and to have something in Ivory responsible for calling Atom’s main tick function.

I ended up resorting to hacks like giving Atom and Ivory variables the same C name and relying on some incidental details of how to refer to functions. This worked, but it was ugly and error-prone, and it also bypassed proper typing. If I mismatched the names, the C code would probably fail to build. If I mismatched the types (for instance, my Atom variable is a uint32_t by way of V Word32 and my Ivory variable is a int16_t by way of Sint16), the generated C code might have had some subtle errors. In either case, Haskell saw no problems in type-checking, because I was only coincidentally coupling the two variables via the generated C code. This could be particularly nasty when I was trying to match pointer types properly, and cheating a little by writing the variable’s name as &foo or *foo.

As an aside, if I remember right, a fair number of the bugs discovered in the code were a direct result of me bypassing the type system in this manner.

Appendix 2: Limitations on Coroutines

Two pernicious limitation I ran into on Ivory’s coroutines were an inability to build up coroutines out of smaller parts, and an inability to take the yield escape hatch that a coroutine provided and pass it around like a first-class value. This wasn’t a slight against them - they are coroutines, behaving like coroutines but inheriting the C-derived limitations that Ivory purposely has, and I was trying to make them behave like something else.

Consider coroutine A and coroutine B. As far as control flow goes, coroutine A can do a few things:

  • return back to caller
  • suspend itself with yield
  • resume coroutine B (or call it in the first place)

(It can’t call itself, but that’s incidental here; Ivory’s coroutines store a continuation in static memory, so only one can be “live” at once.)

However, returning and yielding don’t have any meaningful first-class form. Coroutine A can’t pass its own “return” to coroutine B, and let B return a value to its caller, nor can it pass its own “yield” elsewhere and let another context suspend it.

In other words: these coroutines don’t provide their own continuations or an “exit” continuation; that’s all handled implicitly.

ARMing Haskell http://haskellembedded.github.io//posts/2015-12-15-arm.html 2015-12-15T00:00:00Z 2015-12-15T00:00:00Z Posted on December 15, 2015 by Calvin Beck

I have spent the last few weeks desperately trying to get Haskell working on a Raspberry Pi 2 with Raspbian (Jessie). I have had… some problems

Edit 2015-12-16: Thanks to the help of the wonderful Haskell community, my issues have been resolved. Make sure you have LLVM 3.5.2, or you may encounter the same problems that I did!

Edit 2015-12-17: Thanks to slyfox on #ghc on freenode we now have a sort of working frankenstein’s cross-compiler!


There are a few useful guides available for setting up cross-compilation:

It’s fairly easy to get a cross-compiler up and running, as long as you carefully follow instructions. This is all well and good, but there are still issues with Template Haskell. Template Haskell essentially requires that you can run code built from the compiler on the system running the compiler. Roughly speaking Template Haskell uses Haskell code to generate more Haskell during compilation. Since you can’t run an ARM executable on x86 / x86_64, you can’t compile anything that uses Template Haskell with the cross-compiler as of yet. More on this later, but here’s some more information.

In addition to the lack of Template Haskell, there are problems with certain FFI libraries, like zlib. So, while my 7.10.2 can produce an acceptable ARM “Hello, World!”, I can’t compile my more complicated project. Thus I am forced to look for another option!

Cross-Compilation with QEMU

So, let’s say you have read the section on using a QEMU ARM user chroot with binfmt_misc to run ARM code on your non-ARM machine. If we can 1) have ARM libraries on our machine, and 2) run ARM executables, then it seems like we should be able to run the cross compiler from above, and then when we execute ARM code, drop into qemu-arm.

The only thing we should have to do is tell qemu-arm to load dynamic libraries from somewhere else, so that we can load ARM libraries, and not x86 / x86_64 libraries. Turns out there is an option for this:

$ qemu-arm

-L path       QEMU_LD_PREFIX    set the elf interpreter prefix to 'path'

Yeah, that will work. Using the cross compiler above, and the ARM Gentoo environment set up below I was able to compile my program just fine using:

export QEMU_LD_PREFIX=$HOME/arm-chroot

cabal sandbox init
cabal --with-ghc=arm-unknown-linux-gnueabihf-ghc --with-ghc-pkg=arm-unknown-linux-gnueabihf-ghc-pkg --with-ld=arm-linux-gnueabihf-ld --with-strip=arm-linux-gnueabihf-strip install

Which is AWESOME because the native compiler is so much faster than the one emulated with QEMU. This is not without caveats. For instance when compiling with multiple jobs it took forever and then ran out of memory, setting -j1 with cabal install fixed this particular issue.

A bigger problem is that there appears to be issues with the C FFI. I’m not yet sure how this works, but when I try to run an ARM binary which uses JuicyPixels to write a PNG (which relies upon zlib), I get this error:

user error (Codec.Compression.Zlib: incompatible zlib version)

but otherwise this works surprisingly well.

After a bit of digging I have found that this error comes from here, and since we have got an actual failure, it’s probably from calling the failIfError function. That means our issue is from here.

I have checked the zlib version on all of my environments, and the version is 1.2.8 everywhere. So the version isn’t the issue. In fact if we look at the code for c_deflateInit2_ we’ll notice that it’s only checking the first version number anyway:

if (version == Z_NULL || version[0] != my_version[0] ||
    stream_size != sizeof(z_stream)) {
    return Z_VERSION_ERROR;

But there’s our problem. The size of our z_stream must differ somehow. If we check the Haskell Zlib library we notice the following:

c_deflateInit2 :: StreamState
               -> CInt -> CInt -> CInt -> CInt -> CInt -> IO CInt
c_deflateInit2 z a b c d e =
  withCAString #{const_str ZLIB_VERSION} $ \versionStr ->
    c_deflateInit2_ z a b c d e versionStr (#{const sizeof(z_stream)} :: CInt)

I’m on an x86_64 machine, so it’s pretty much guaranteed that the z_stream structure on my machine differs in size to the one on the 32 bit ARM machines. This should be processed by hsc2hs, so that’s where the issue is. I need to be running an hsc2hs that targets ARM, not my native one. I had an arm-unknown-linux-gnueabihf-hsc2hs, but it seemed to loop forever, as did the hsc2hs from my chroot (but not when running it in my chroot). So that’s no good either.

hsc2hs by default generates a C program, which when run spits out the appropriate Haskell file. So we just need to get hsc2hs to generate ARM code. I can pass hsc2hs options with cabal, which means I can tell the native hsc2hs to compile using a cross compiler and linker.

--hsc2hs-option="-c arm-linux-gnueabihf-gcc -l arm-linux-gnueabihf-ld"

Unfortunately that still doesn’t work! We’re on the right track, but not quite there yet. The problem now is that arm-linux-gnueabihf-ld doesn’t actually know where to look for libc (we need the ARM one). We can use the --sysroot option to make it use the ARM chroot. I actually had to change to gcc for the linker as well, because it handles linking with the C runtime much more nicely.

--hsc2hs-option="-c arm-linux-gnueabihf-gcc -l arm-linux-gnueabihf-gcc -C "--sysroot=$HOME/arm-chroot/" -L "--sysroot=$HOME/arm-chroot/""

This loops forever with qemu-arm, however the executable when run on the Raspberry Pi 2 works perfectly fine. This seems to be a QEMU bug.

Note that hsc2hs actually has cross compilation options (-x). When these are used instead of creating a C program hsc2hs uses tricks to figure out what’s going on with the target. Unfortunately this doesn’t handle const_str, which we need, so this won’t work for us.

Running on the Raspberry Pi

Raspbian has an old version of GHC in its repos, GHC 7.6.3, which works with simple pieces of code. For instance “Hello, World!” might compile and run perfectly well. However, my small image processing program encountered nasty, randomly changing, run time errors, and segmentation faults. Sometimes, if the stars aligned, the program would run to completion producing correct results, other times it seemed to loop forever. This is not good. One such error that I received was:

allocGroup: free list corrupted

which, if we look at the source code, should definitely never happen. Everything that is happening here SCREAMS that memory is getting stomped on somewhere. This is not something which is going to be easy to debug as the problem could quite literally be anywhere in the code, or in fact in a different library entirely. Not good.

What about a newer compiler?

So, the Raspbian compiler is horribly ill, and we have to try something different. I attempted to compile GHC from scratch, but this is an effort which takes a very long time on a Raspberry Pi, and after fixing build errors I still had issues. Fortunately since GHC 7.10.2 there are binaries for ARMv7. Additionally, I found a guide which suggested that there were no issues on a Scaleway server:


Following these suggestions I was able to install 7.10.2, and 7.10.3 on the Raspberry Pi. Unfortunately these compilers have given me quite a bit of grief, as I am incapable of producing a working “Hello, World!” with them (despite the 7.10.2 cross-compiler working just fine for this):


Cabal-install hangs, and this too is a dead end for me.

Or it would be if it wasn’t for Ben Gamari, who replied to my issue in the GHC trac. As it turns out the LLVM version available with Raspbian is 3.5.0. This version has an issue on ARM which breaks the binaries that GHC spits out. Upgrading to 3.5.2 should fix this problem!


QEMU is an attractive option. We can emulate an ARM machine on a fast x86 processor, which may be faster. At any rate it’s nice to be able to compile, and even test ARM binaries, on your development system, without having to dedicate a Raspberry Pi as a build bot. I only have access to one Raspberry Pi 2 at the moment, and it’s occupied with work stuff. QEMU would make things easier, and hell, it might even work.

QEMU System Emulation

This is also a dead end. I am horrendously bad at getting QEMU machine emulation to work. I got it working with Raspbian Wheezy, but it wouldn’t work with Jessie for some reason. I spent a lot of time trying to get an ARM machine emulated, but all of the guides are filled with archaic options, vmlinuz kernels, and magic. Ultimately nothing worked, and this was a huge waste of time that would be slow anyway. Here be dragons. All who dare enter should beware.

QEMU User Emulation

Initially I thought that system emulation would be much easier to set up and get working than user emulation. I was wrong. QEMU system emulation will emulate an entire ARM machine, whereas user emulation essentially just lets you run ARM binaries on a different machine as a regular user process. User emulation translates all of the instructions, and sys-calls, but uses the same kernel and filesystem as before. This is cool. What’s especially cool is that Linux has a feature called binfmt_misc, which lets you run arbitrary executable formats. So, we can actually get our normal x86 / x86_64 Linux system to transparently execute ARM binaries. Essentially we use binfmt_misc to tell the kernel to run ARM executables with the qemu-arm program. This is pretty awesome.

There are some interesting possibilities with this, as we might be able to leverage this to make the cross compiler work with Template Haskell. After turning this on, instead of getting Exec format error’s with Template Haskell and the cross compiler, it was instead complaining about missing ARM libraries. Cool. This is something that might be worth exploring at a later date, but I don’t really want to mess with mixing ARM and x86_64 binaries on my computer. That’s bad mojo. Worth messing with in the future, because it has the possibility of being faster, but it’s probably filled with caveats and it seems a bit scary.

So, what’s the next best option? How about a chroot!? Yeah. That’ll work. So, here’s the plan! In order to make sure we get all of the ARM libraries we need, we’ll just install an ARM Linux distribution in a chroot, and use binfmt_misc and qemu-arm to transparently execute any ARM binaries in the chroot. I got some information for how to set up binfmt_misc on Gentoo here:


This guide seems to be doing more complicated stuff with LXC, which I don’t really understand, so I have deviated and just went with a simple chroot Linux install. I’m going to install Gentoo, because it’s what I know, and I find that it doesn’t hide problems from me, and it will let me try different versions of LLVM and other libraries which might be causing problems quite easily.

We need access to qemu-arm in our chroot if we want to use it to run ARM binaries. The simple way to do this is to statically link qemu-arm, which will allow us to copy the qemu-arm binary into the chroot, and not have to worry about copying any dynamically loaded libraries as well. In order to do this on Gentoo we simply add the static-user use flag to the qemu package, your distro may vary. We can check that we are good to go with ldd:

$ ldd `which qemu-arm`
    not a dynamic executable

Looking good! Make sure you set up binfmt_misc first, but now we can make our chroot.

# First we make the directory for our chroot:
mkdir ~/arm-chroot
cd ~/arm-chroot

# Get the Gentoo stage3
wget http://distfiles.gentoo.org/releases/arm/autobuilds/20151116/stage3-armv7a_hardfp-20151116.tar.bz2
tar -xjf stage3-armv7a_hardfp-20151116.tar.bz2

# Copy qemu-arm into the chroot, so we can use ARM binaries when chrooted.
cp `which qemu-arm` ~/arm-chroot/usr/bin/qemu-arm

# Then we do the magical mounting: https://wiki.gentoo.org/wiki/Handbook:AMD64/Installation/Base#Mounting_the_necessary_filesystems
mount -t proc proc proc
mount --rbind /sys /sys
mount --make-rslave sys
mount --rbind /dev dev
mount --make-rslave dev

# And now we chroot!
sudo -s
chroot . /bin/bash

# At this point you can pretty much just follow the Gentoo Handbook https://wiki.gentoo.org/wiki/Handbook:AMD64/Installation/Base#Configuring_Portage
emerge --sync

# ...
# Configure the system how you want...
# ...

# Note that we need LLVM version 3.5.2, which you may need to add to package.accept_keywords
echo "=sys-devel/llvm-3.5.2 **" >> /etc/portage/package.accept_keywords

# Now we can install whatever we need for GHC, like LLVM
emerge -a llvm binutils zlib

# Grab and install GHC ARMv7 binaries...
wget http://downloads.haskell.org/~ghc/7.10.3/ghc-7.10.3-armv7-deb8-linux.tar.bz2
tar -xjf ghc-7.10.3-armv7-deb8-linux.tar.bz2
cd ghc-7.10.3
make install

The first time I did this I still encountered the same problem as on the Raspberry Pi with the qemu-arm GHC, however after installing LLVM 3.5.2 I have had no more problems. You can even install Cabal and cabal-install pretty easily. Just download the tarballs from here, and follow the instructions in the README files. It really is that simple. Make sure to move the cabal executable somewhere in your path, and run cabal update, and then you should be set!

I have since been able to compile my image processing program, and stuff it on the Raspberry Pi 2. No problems at all. QEMU is a bit slow, but it’s nice to not have to worry about compiling on the Pi, and now I can do everything from my development machine. This is quite a bit slower than the Pi 2 itself, but works very well.

Current Status

After much pain and suffering I have a way to do Haskell development on ARM! Others have had success come quite a bit more easiely. I have had a conversation with somebody on Twitter whom found success with Scaleway servers and a Beaglebone Black. The difference here seems to be that whatever image they were using on Scaleway had LLVM 3.5.2, and not the broken LLVM 3.5.0.

Good luck to anybody trying to do the same! Ask questions, or boast about your success in the comments.

The Future

So with that done and working, here’s some stuff that could greatly improve the Haskell on ARM development experience:

  • It would be really nice to have binary packages for ARM, which is something that nix could provide. Anthony Cowley thinks this is a good idea too.
  • It might be possible to build a GHC cross compiler, and have it transparently execute ARM binaries with binfmt_misc and qemu-arm for Template Haskell.
    • There would still be caveats.
    • This would be much faster than emulating the compiler, though.
    • Perhaps there is a way to get qemu-arm to use a different path for dynamic libraries, so you can have ARM libraries somewhere nice and separate.
  • Gentoo Prefix might be a bit nicer than a chroot.
  • Stack currently has issues on ARM. It would be nice to get Stack working somehow.
Embedding Haskell: Compilers, and compiling compilers http://haskellembedded.github.io//posts/2015-10-09-compiler-compilers.html 2015-10-09T00:00:00Z 2015-10-09T00:00:00Z Posted on October 9, 2015 by Chris Hodapp

My last post mentioned that some things need some better explanation, because I’m always trying to re-explain and clarify.

This blog is devoted to the use of Haskell with embedded systems. What does that even mean? We see a couple broad categories (which the slides on the last page, as well as our Links page, mirror):

  1. Full Compilation: Compiling Haskell code to an embedded target.
  2. Limited Compilation: Compiling some limited subset of Haskell code to an embedded target.
  3. Hosted EDSL & Compiler: Hosting, in Haskell, an EDSL and a compiler to an embedded target.

As far as I know, I made these categories up. If anyone happens to know a more established classification, better names, or an example of who wrote about it first, please tell me.

This might look like a lopsided, arbitrary grouping; it sort of is. The commonality is that in all cases one uses Haskell to express something (a program, a circuit, specifications, call it what you will) for an embedded target. More on that follows.

I exclude things like Cryptol and Idris from this because - while implemented in Haskell and usable for embedded platforms - they are different languages unto themselves. I might arbitrarily drop that distinction in the future if I feel like it…

Full Compilation

This is what normally comes to mind when people hear about using Haskell with embedded systems - compiling the Haskell code to run directly on an embedded target, bringing along the normal runtime with it (plus whatever required bootstrapping and support). The Compiling to Embedded Targets section of the Links page is concerned particularly with this.

However, this actually appears to be pretty rare. The nature of the Haskell language brings some formidable challenges. Particularly, one must make the Haskell runtime fit on the target and make the garbage collection and lazy evaluation behave in predictable and sane ways.

Ajhc, a JHC-derived compiler from Kiwamu Okabe of METASEPI, is the only example of this I found - it could compile and execute on ARM Cortex-M3/M4. Kiwamu has written a lot on his experiences with making Haskell run in this footprint. His subsequent switch to the ATS language may be a hint.

HaLVM from Galois might arguably fit in this category.

Limited Compilation

This uses an existing compiler for certain stages (such as the parsing and type-checking), but a custom back-end to actually produce code, often with a lot of static analysis. This may adapt or disallow certain constructs (for instance, floating-point, recursive functions, recursive datatypes: CλaSH Unsupported Haskell features).

GHC accomodates this by allowing developers to invoke GHC functionality, from Haskell, as a library.

The Compiling for FPGA/ASIC section of the Links page has a few examples of this.

Hosted EDSL & Compiler

The Code Generation EDSLs and Circuit Design EDSLs sections of the Links page cover the copious examples of this. Atom, the topic of a few of my prior posts, is in this category.

This category is the one I am most often having to explain. It typically uses an EDSL (embedded domain-specific language) inside of Haskell to direct the process of code generation to a lower-level representation. This is otherwise called: compiling.

To emphasize: The code that runs on the target is entirely decoupled from the Haskell runtime. The Haskell compiler here isn’t compiling anything for the target - it’s compiling another compiler and the input to that compiler. That input happens to be specifications of what will run on the target.

This is a limitation of one sort:

  • Basically all notions of ‘runtime’ on the embedded target must be handled separately. (Ivory works with this still, for instance with the Num typeclass, in some surprising ways. More on that will follow in a future post!)
  • This adds the confusion and complication of another stage (possibly multiple stages) to the process of bringing code/specifications to the embedded target. This is why I use Shake.

It’s also a benefit of another sort:

  • Any Haskell environment compatible with the libraries in question should produce the same results (as far as the embedded target cares). Its runtime does not matter, nor whether the environment has any knowledge of the architecture of the embedded target.
  • That stage separation also adds a nice opportunity for static analysis and optimization. For instance, Copilot makes use of this to add an interpreter/simulator, SBV uses it to prove or disprove given properties about the code, and Atom uses it to verify some timing constraints.

I said in the last post that in this category Haskell takes on the role of a metaprogramming or template language. While this may be true, I sort of ignored that it’s less relevant, because it’s the same in all the other categories.


Lumping together these categories might seem like a stretch, especially considering that the last category involves extra stages and a shift in how one thinks about the software.

Ponder the following, though:

  • A “normal” Haskell program interacts through what is sequenced in the famous IO monad (particularly, the value called main).
  • An Atom specification interacts through what is sequenced in the Atom monad (particularly, whichever values one passes to the Atom compiler).
  • An Ivory program interacts through what is sequenced in the Ivory eff and Module monads (particularly, whichever values one passes to the Ivory compiler).
  • A CλaSH description interacts through the Signal applicative (particularly, the value called topEntity).

Is a trend clear? (No, it’s not monads. Signal is only applicative, and I suspect Lava behaves similarly.)

That list spans our three categories. In each of them, one builds up a program (in a very broad sense) simply by building up a value in Haskell. Beyond that, the only real differences are,

  • the type of that value,
  • what system handles it (the Haskell compiler and runtime, some other compiler and maybe runtime, or a combination thereof),
  • and the eventual output (native binary, LLVM bitcode, C code, VHDL code, assembly language, input to a model checker, etc.).

Ignoring the vague nature of the term, “declarative,” this relates pretty directly to the declarative nature of Haskell programs.

Seen from this perspective, one is still compiling Haskell to run on some embedded target. The compilation just might continue outside of the system’s Haskell compiler, and the running might not involve its runtime.

Presentation at CincyFP http://haskellembedded.github.io//posts/2015-06-09-atom-cincyfp-slides.html 2015-06-09T00:00:00Z 2015-06-09T00:00:00Z Posted on June 9, 2015 by Chris Hodapp
Tags: haskell, atom

Later note: This post is back-dated because while I’d put the slides in the repository already, I had not actually linked to them or said anything about them.

The fine people at CincyFP, the local (to me) functional programming group, requested that I give a presentation on some of the embedded Haskell stuff I was doing, and I did this at the June meeting this year.

Slides from the presentation are up here (and Markdown source; or look in the repo). CincyFP seems to have mostly Clojure aficionados, so in terms of Haskell-heavy details I kept this presentation as a “part 1” to some possible future presentations. Actually, not even that, since the title was “EDSLs & Metaprogramming” and I only scratched the surface of that.

I start walking through an Atom example at slide 9. While I live-coded this at the presentation, I have no video or audio. However, I put my example code online here (and StringEmbed.hs).

The slides are fairly terse, and I intend to explain bits of them in the next few posts. Particularly, around slide 2, I try to explain a few different broad ways Haskell might be used on embedded systems, and this refers to similar categories as on the Links page. I find myself having to explain these distinctions quite often, so I am going to try to explain this better in posts to come.

Slide 6 is a little bit misleading. The next post tries to patch this up a bit.

How I Got Here (i.e. to using Haskell for embedded code) http://haskellembedded.github.io//posts/2015-02-06-how-i-got-here.html 2015-02-06T00:00:00Z 2015-02-06T00:00:00Z Posted on February 6, 2015 by Chris Hodapp

One work project since near the begining of 2014 has been the design of an embedded system for which power usage and stability are two primary concerns. It’s not controlling an airplane or a nuclear plant - malfunctions will not be catastrophic - but stability still matters.

My boss had decided that for various reasons too numerous and extensive to list here, we needed to have support for Bluetooth Low Energy. Our system at the time ran on the venerable TI MSP430 and I started looking at ways to support BLE from this. All of TI’s BLE offerings at the time ran on the 8051 and appeared to require proprietary toolchains. After surveying what else was available, we had eventually decided on the Nordic nRF51822, a microcontroller based on an ARM Cortex-M0, supported by standard GCC, and providing all the necessary peripherals for BLE - and simply eliminated the MSP430 altogether.

It quickly evolved to a distributed system - some parts were sensors or actuators that were BLE peripherals, another part ran constantly as a BLE central, another part ended up as a more powerful, Internet-connected Linux machine that ran only sparingly.

A few patterns emerged:

  • All parts needed to be speaking the same protocol, which necessitated keeping various structures and constants in sync at the software each part ran.
  • The nRF51822 board acting as the BLE central was responsible for juggling a lot of concurrent operations, because nearly all API calls were async.
  • The nRF51822 boards ran different software, but still shared various bits of code and constants.

The two languages here were C for the nRF51822, and Python for the Linux machine. I tried to build abstractions that could sensibly represent these patterns, but were sufficiently lightweight in C. One was in Python to keep data types in sync; for Linux, it handled it at runtime in Python, and for the microcontroller, it generated C code with the requisite memcpy calls and proper offsets and lengths. The C code also had various FSMs (some explicit, some not) for managing the concurrent operations. At later examination they were nearly all ad-hoc coroutines that were ‘hiding’ a very simple concurrent description in their details.

Seeing that I had ad-hoc coroutines hidden everywhere in my code, I tried to integrate in some lightweight RTOSes that provided some form of cooperative thread or coroutine. I looked at Atomthreads, RIOT OS, Contiki, FreeRTOS, and ChibiOS/RT, but the issue that stopped me in all cases was that they appeared they would interfere with Nordic’s firmware, which I required for the Bluetooth Low Energy functionality. Finally, I discovered cocoOS which provided just the cooperative threads and basic messaging primitives, and due to its simplicity required only minimal implementation and nothing very low-level. I quickly ported it and it was working seemingly wonderfully.

I had recently read Joe Armstrong’s famous thesis on Erlang, and found it very cogent and pragmatic, but still accessible. He defines on page 19 Concurrency Oriented Programming. I had a thought that perhaps cocoOS gave me the primitives I needed to let me apply the methodology that Armstrong described, and express the system as a design around concurrent processes. With clean system design in hand and hopeful visions of elegance in my head, I set about working on this - until reaching an abrupt ending when I ran out of memory with around 2 cooperative tasks and almost nothing else compiled in.

Around the same point, I had also extended my Python code generation to generate code for some more complex protocols and refactored it to make use of a very handy library, Cog.

At some point I saw that these all were sides of the same ugly dilemma (trilemma?):

  • I could write larger amounts of code that would ‘hide’ the simpler representations inside.
  • I could attempt to streamline the above with code generation via macros.
  • I could build or use runtime abstractions that helped me approximate those simpler representations, but incurred too much overhead.

#define and #include existed, but they addressed only the smallest of cases, and I felt like C++ was no cure either. Cog helped streamline the code generation, but my code generation still felt like primitive macros. My view of code generation in general was grim too, from seeing its use at other jobs. In particular:

  1. The need for automatically-generated code probably means that the underlying language lacks the right abstractions (or that you do not understand them).
  2. Either you incur the complexity of implementing the code generation in that same (lacking or ill-understood) language, or you incur the mental overhead of having to coordinate with another language at the same time - possibly a third language, if you handle specifications in a separate language.
  3. You don’t fix a problem in automatically-generated code - you fix the code generator or the specifications, which is nearly always more difficult and has more consequences.
  4. The code generator’s scope tends to expand anywhere generated code touches manually-written code.

Of course, avoiding code generation completely is senseless. Compilers are code generators. They run on CPUs probably created (gate-wise) by some form of code generator. The problem is not code generation, but code generation as ad-hoc automation that buries complexity underneath a layer of fresh complexity.

Luckily, plenty of people (besides compiler writers) seem to get code generation right. After my failure to make any progress with cocoOS, I had started reading about Atom, an EDSL in Haskell which generates C code for hard realtime embedded software. It looked very promising and solid, but too narrow in scope for what I needed. Shortly after, I found Copilot, another Haskell EDSL for some similar purposes which generates C either via Atom or SBV (also a Haskell EDSL). Experience Report: a Do-It-Yourself High-Assurance Compiler from NASA focuses on Copilot, but identifies some general benefits from the paradigm; it is a short, informative read that I highly recommend.

I stumbled into Ivory from Galois Inc. (another Haskell EDSL, of course) and knew quickly that I had found something very powerful for my own use-case. Their experience report is a quick read, but a good summary of Ivory (as well as Tower, yet another Haskell EDSL). It’s still a rather young project, and documentation and examples are sparse. However, it is under active development, and its developers (particularly Lee Pike, who I’ve bothered with plenty of emails) have been very responsive to my inquiries.

(To be clear, these all are Haskell EDSLs oriented to code generation. All of them in some fashion allow the programmer to express a specification within Haskell, and then generate C code at runtime. Haskell code is not actually being built for any embedded target - although, some authors here had interest in doing this via JHC, and the Idris language extracts the entire runtime and program to C with some recent work going into making this light enough for embedded targets. A certain Dr. Franco at my university insisted to me several years ago that code generation from a specification was the way of the future, and was most pleased when I suggested this year that perhaps he was correct.)

After some more reading and examination here, I started migrating the code over to a combination of Atom and Ivory. Atom quickly proved useful for managing a lot of the concurrency that was present, and generally handling high-level scheduling. The transition from C code to Ivory was rough in spots, but Ivory proved very useful too for representing all kinds of general functionality.

Haskell’s power as a language has been proving immensely useful here. Effectively, the EDSLs have moved the level of meaningful abstraction up into code-generation, and this has both given me much better abstraction and let me eliminate some runtime overhead.

More in-depth examples and explanations on things like Atom, Copilot, Ivory, and SBV will follow on this blog.



  1. Armstrong, J. Making reliable distributed systems in the presence of software errors. http://www.erlang.org/download/armstrong_thesis_2003.pdf
  2. Pike, L., Wegmann, N., Niller, S., & Goodloe, A. (2012). Experience Report: a Do-It-Yourself High-Assurance Compiler. http://ntrs.nasa.gov/archive/nasa/casi.ntrs.nasa.gov/20120014570.pdf
  3. Hickey, P. C., Pike, L., Elliott, T., Bielman, J., & Launchbury, J. (2014) Building Embedded Systems with Embedded DSLs (Experience Report). ACM 978-1-4503-2873-9/14/09. https://github.com/GaloisInc/smaccmpilot-experiencereport/blob/master/embedded-experience.pdf?raw=true


  1. cocoOS http://www.cocoos.net/intro.html
  2. Cog: Python Success Stories https://www.python.org/about/success/cog/
  3. atom: A DSL for embedded hard realtime applications. http://hackage.haskell.org/package/atom and https://github.com/tomahawkins/atom
  4. sbv: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. https://hackage.haskell.org/package/sbv and https://leventerkok.github.io/sbv/
  5. copilot: A stream DSL for writing embedded C programs. http://hackage.haskell.org/package/copilot and https://leepike.github.io/Copilot/
  6. Ivory, an eDSL for safe systems programming. http://ivorylang.org/ and https://github.com/GaloisInc/ivory
  7. Jhc Haskell Compiler. http://repetae.net/computer/jhc/
Haskelly Beginnings http://haskellembedded.github.io//posts/2015-01-31-haskelly-beginnings.html 2015-01-31T00:00:00Z 2015-01-31T00:00:00Z Posted on January 31, 2015 by Calvin Beck

Greetings, all!

This is the start of a project to expand Haskell’s reach in the embedded world. At the moment we are simply exploring some of the available options, and we hope to expand on the documentation, and examples that are available. Here’s a list of some of the things which we are aware of? Got anymore? Let us know!

We’ll have a better idea of what’s going on with this soon. Right now this is essentially just a test of our super cool Hakyll blog using GitHub Pages

You can find the source for this blog here!