Links

Posts reference these links in context, but they are still useful in a central spot.

Code Generation EDSLs

• Ivory (hackage, GitHub repo) is a more general EDSL from Galois “for safer systems programming”. Ivory is still quite young, but looks very promising.
  • This experience report is probably the best introduction: Building Embedded Systems with Embedded DSLs (Experience Report)
  • Their GitHub repo contains a paper that is still a work-in-progress.
  • Our own Ion library (see the Introducing Ion post) targets Ivory.
• Copilot (hackage) is a “stream language for generating hard real-time C code” also from Galois. Documentation on Copilot is excellent.
  • This report from NASA gives a good explanation: Experience Report: a Do-It-Yourself High-Assurance Compiler
  • Copilot has backends for both Atom and SBV. Anthony Cowley’s talk at NYHUG, Abstractions for the Functional Roboticist (& slides PDF), talks about both Copilot and SBV, among other things.
• Atom (GitHub repo) is a language from Tom Hawkins for hard realtime embedded software.
  • Documentation and examples are rather limited, but our few posts on Atom compile nearly everything we know on it.
• SBV (GitHub repo, GitHub page) is more specific to SMT-based verification in Haskell, but also generates verified C code. Documentation and examples on SBV are excellent.

Circuit Design EDSLs

• Lava is an entire family of Haskell-based EDSLs unto itself, but the seminal 1998 paper appears to be Lava: Hardware Design in Haskell - which defines it as “a tool to assist circuit designers in specifying, designing, verifying and implementing hardware.”
  • One of its authors, Satnam Singh, has a blog entry on it as well: The Lava Hardware Description Language.

Compiling for FPGA/ASIC

• From Christiaan Baaij is CλaSH: CAES Language for Synchronous Hardware (GitHub, hackage and its associated tutorial. CλaSH is a “functional hardware description language that borrows both its syntax and semantics from the functional programming language Haskell.”
  • Note in the “CλaSH vs Lava” section in the tutorial that CλaSH is not an EDSL like the Lava family, but rather, it uses a static analysis approach.
  • arjanb pointed us to CλaSH FPGA Starter, a quick tutorial for the Terasic DE0-Nano. (Alternate link)
  • QBayLogic, a company which Christiaan co-founded, provides consulting for CλaSH.
• The Reduceron is some very interesting work with an FPGA softcore for running lazy functional programs.
  • It was forked/revived as a newer project (GitHub).
• Conal Elliott worked with a Silicon Valley startup, Tabula, on massively-parallel execution of Haskell code on a new FPGA-ish architecture (Spacetime), using an approach based on Cartesian Closed Categories. They’re now defunct, as far as I know, but supposedly trying to open-source some components. I’m aware only of lambda-ccc.

Compiling to Embedded Targets

• The Jhc-based Ajhc compiler (GitHub, Hackage) is a now defunct-project, but seemed to have the aim of compiling Haskell to various other platforms (especially given their “Haskell everywhere” tag).
  • Ajhc demo for Cortex-M3/4 board gives their example of compiling Haskell to an ARM Cortex M3/M4.
  • The 2014 paper Metasepi Report: Writing NetBSD Sound Drivers in Haskell: A Reentrant Haskell Compiler for Operating Systems Programming from Kiwamu Okabe (METASEPI) and Takayuki Muranushi (Kyotu University) talks about the experiences and challenges with using a Haskell compiler for targeting embedded code.
  • Kiwamu Okabe has a number of presentations up at SlideShare about his work with METASEPI and Ajhc.
• From fpcomplete is inline-c, which “lets you seamlessly call C libraries and embed high-performance inline C code in Haskell modules”. This isn’t specifically for embedded, of course, but it certainly has application there. (Thank you to @matrixai for pointing this out.)

Not Haskell per se, but Haskell-inspired and Haskell-hosted

• Idris (hackage) is a language from Edwin Brady, “a general purpose language with full dependent types.” It is a recent language, but still has many good papers, talks, and references.
  • The paper from Brady & Hammond, Resource-safe Systems Programming with Embedded Domain Specific Languages, explains a particular application of Idris that looks very practical.
• Cryptol is yet another Galois creation, a DSL for specifying cryptographic algorithms.
• HaSKI is “an FPGA-based SKI calculus evaluator written in Haskell/Cλash”. Thank you to arjanb for pointing this one out.