announcing arduino-copilot

arduino-copilot, released today, makes it easy to use Haskell to program an Arduino. It's a FRP style system, and uses the Copilot DSL to generate embedded C code.

gotta blink before you can run

To make your arduino blink its LED, you only need 4 lines of Haskell:

import Copilot.Arduino
main = arduino $ do
    led =: blinking
    delay =: constant (MilliSeconds 100)

Running that Haskell program generates an Arduino sketch in an .ino file, which can be loaded into the Arduino IDE and uploaded to the Arduino the same as any other sketch. It's also easy to use things like Arduino-Makefile to build and upload sketches generated by arduino-copilot.

shoulders of giants

Copilot is quite an impressive embedding of C in Haskell. It was developed for NASA by Galois and is intended for safety-critical applications. So it's neat to be able to repurpose it into hobbyist microcontrollers. (I do hope to get more type safety added to Copilot though, currently it seems rather easy to confuse eg miles with kilometers when using it.)

I'm not the first person to use Copilot to program an Arduino. Anthony Cowley showed how to do it in Abstractions for the Functional Roboticist back in 2013. But he had to write a skeleton of C code around the C generated by Copilot. Amoung other features, arduino-copilot automates generating that C skeleton. So you don't need to remember to enable GPIO pin 13 for output in the setup function; arduino-copilot sees you're using the LED and does that for you.

frp-arduino was a big inspiration too, especially how easy it makes it to generate an Arduino sketch withough writing any C. The "=:" operator in copilot-arduino is copied from it. But ftp-arduino contains its own DSL, which seems less capable than Copilot. And when I looked at using frp-arduino for some real world sensing and control, it didn't seem to be possible to integrate it with existing Arduino libraries written in C. While I've not done that with arduino-copilot yet, I did design it so it should be reasonably easy to integrate it with any Arduino library.

a more interesting example

Let's do something more interesting than flashing a LED. We'll assume pin 12 of an Arduino Uno is connected to a push button. When the button is pressed, the LED should stay lit. Otherwise, flash the LED, starting out flashing it fast, but flashing slower and slower over time, and then back to fast flashing.

{-# LANGUAGE RebindableSyntax #-}
import Copilot.Arduino.Uno

main :: IO ()
main = arduino $ do
        buttonpressed <- input pin12
        led =: buttonpressed || blinking
        delay =: MilliSeconds (longer_and_longer * 2)

This is starting to use features of the Copilot DSL; "buttonpressed || blinking" combines two FRP streams together, and "longer_and_longer * 2" does math on a stream. What a concise and readable implementation of this Arduino's behavior!

Finishing up the demo program is the implementation of longer_and_longer. This part is entirely in the Copilot DSL, and actually I lifted it from some Copilot example code. It gives a reasonable flavor of what it's like to construct streams in Copilot.

longer_and_longer :: Stream Int16
longer_and_longer = counter true $ counter true false `mod` 64 == 0

counter :: Stream Bool -> Stream Bool -> Stream Int16
counter inc reset = cnt
   where
        cnt = if reset then 0 else if inc then z + 1 else z
        z = [0] ++ cnt

This whole example turns into just 63 lines of C code, which compiles to a 1248 byte binary, so there's plenty of room left for larger, more complex programs.

simulating an Arduino

One of Copilot's features is it can interpret code, without needing to run it on the target platform. So the Arduino's behavior can be simulated, without ever generating C code, right at the console!

But first, one line of code needs to be changed, to provide some button states for the simulation:

        buttonpressed <- input' pin12 [False, False, False, True, True]

Now let's see what it does:

# runghc demo.hs -i 5
delay:         digitalWrite_13: 
(2)            (13,false)    
(4)            (13,true)     
(8)            (13,false)    
(16)           (13,true)     
(32)           (13,true)

Which is exactly what I described it doing! To prove that it always behaves correctly, you could use copilot-theorem.

peek at C

Let's look at the C code that is generated by the first example, of blinking the LED.

This is not the generated code, but a representation of how the C compiler sees it, after constant folding, and some very basic optimisation. This compiles to the same binary as the generated code.

void setup() {
      pinMode(13, OUTPUT);
}
void loop(void) {
      delay(100);
      digitalWrite(13, s0[s0_idx]);
      s0_idx = (++s0_idx) % 2;
}

If you compare this with hand-written C code to do the same thing, this is pretty much optimal!

Looking at the C code generated for the more complex example above, you'll see few unnecessary double computations. That's all I've found to complain about with the generated code. And no matter what you do, Copilot will always generate code that runs in constant space, and constant time.

Development of arduino-copilot was sponsored by Trenton Cronholm and Jake Vosloo on Patreon.