Erlang code generator for Idris 2

I want to share a project that I have worked on for 1,5 years: Erlang code generator for Idris 2. The Erlang code generator makes it possible to run Idris 2 programs on the BEAM, and it provides great interoperability with Erlang/Elixir (and other BEAM languages).

The Erlang code generator is still under development, but it is working well enough to try out. At the end of this post I have added links to the biggest remaining issues regarding the Erlang code generator.

An 11 minutes long video showing the Erlang code generator in action: https://www.youtube.com/watch?v=lXtSddDoQ4g
(Sorry for the low production quality, but I hope it gets the point across)

About Idris 2

Idris 2 describes itself as: A purely functional programming language with first class types. The development of Idris 2 is led by Edwin Brady. You can read more about it at https://www.idris-lang.org and https://github.com/idris-lang/Idris2

Why Idris 2?

Here is why I am interested in Idris 2:

  • Focus on interactive editing
    • The compiler should be your assistant, not your adversary
  • Can provide many guarantees [1]
    • Referential transparency
      • Functions that perform side-effects have to be annotated as such.
    • Dependent types
      • By allowing arbitrary values in the types, the types can be made more precise.
    • Total functions
      • The compiler can check that a function is total, which means that the function won’t crash or go into an infinite loop.
        • Note that the compiler is not able to check this property for all total functions. In some cases you may need to write the function in a different way or possibly assert that it is total (Note that you should be careful about such assertions: If the assumption is wrong, it may cause run-time errors).
    • Quantitative type theory
      • Can be used for:
        • Decide which values/types are available at run-time
        • Create messaging protocols with linear types
  • Meta-programmering
    • Can be used for:
      • Generate lots of functions from a small description (like a HTML DSL)
      • Create efficient routes lookup
      • Generate an implementation of interfaces (like Eq, Ord) for data types (Similar to deriving in Haskell)
      • Automate proofs
  • Supports multiple code generators
    • The following are included: Chez Scheme, Racket, Gambit Scheme and JavaScript
    • Now also supports Erlang! (Needs to be installed separately)

Even though Idris 2 can provide many guarantees, that doesn’t mean that you have to write all code to abide by these rules. Maybe it makes sense to allow parts of your program to be partial. The nice thing about this is that Idris 2 will warn you if you try to call a partial function from a function that is annotated as total.

[1] The guarantees rely on some assumptions. Wrong use of unsafe functions may cause run-time errors, for example when doing interop with the host language. Another example: Given a function that has been checked to be total, if this function is calling functions in modules that are not available at run-time, it may still fail. Additionally, there might be bugs in the compiler, the code generator or in the libraries, resulting in run-time errors. Luckily, Erlang is equipped to handle such events.

Why build the Erlang code generator?

My goal is to build web sites/services in Idris 2, and I knew that I would not be able to build everything from scratch in Idris 2. Thus, having access to functionality from another platform is crucial. I have previously worked with Elixir and Phoenix Framework (which was a nice experience), and I like how concurrency works in Erlang, so I decided to make an Erlang code generator.

What functionality does the Erlang code generator provide?

  • Compile Idris 2 programs to Erlang source code or compile to BEAM (via erlc)
    • Basic support for separate compilation. Use together with mix_idris2 to automatically recompile changed modules.
  • Erlang interop
    • Almost all of Erlang’s data types have a corresponding type in Idris.
    • Call almost any Erlang function from Idris.
    • Export Idris functions to be called from Erlang code.
    • Includes decoding functions to safely convert untyped Erlang values to typed Idris values.
  • Supports most of the functionality provided by Idris 2’s base package. (Currently a few modules are placed in the Erlang namespace)

Another notable thing about Idris 2 is that it is self-hosting. In other words, Idris 2 is written in Idris 2. Combining that with the support for custom code generators, it is possible to make the Idris 2 compiler run on many platforms (provided that the code generator implements the necessary primitives). The Erlang code generator has done exactly that, and the Idris 2 compiler is available as a package on Hex. (Note: Idris 2 running on Erlang is currently much slower than Idris 2 running on Chez Scheme. See the remaining issues at the bottom.)

There is also Mix compiler (on Hex) that will help with compiling Idris 2 code in an Elixir project.

Interoperating with Erlang

Calling an Erlang function

Here is an example of how to call a function in Erlang, namely lists:reverse/1:

reverseList : List Integer -> List Integer
reverseList xs = erlUnsafeCall (List Integer) "lists" "reverse" [xs]

The above example restricts the list to the Integer type. It is also possible to write a generic version of this function (With type signature List a -> List a): samples/2-FFI/Main.idr.

Erlang maps

Because Idris 2 supports dependent types, it is possible to include values in the types. This is demonstrated in the data type ErlMapSubset, which is used to represent Erlang maps.

A concrete example: The type ErlMapSubset ["name" := String, "age" := Integer] represents any Erlang map that contain at least the following keys/values: <<"name">> with a binary value, and <<"age">> with an integer value. To retrieve a value from this type, you can call get "name" which will return a String. If you want to retrieve a key that is not specified in the type, you can use lookup. However, this function returns a Maybe type because the key might not exist.

More code samples

Remaining issues

The biggest remaining issues regarding the Erlang code generator:

Wrapping up

This is still the early days of Idris 2 and the Erlang code generator. If you try them out, be aware that you might encounter unimplemented functionality or bugs.

Let me know if you have any questions about the Erlang code generator or Idris 2 in general.

17 Likes

Awesome project! Thank you for sharing!

1 Like

I am very excited by this. I love the concepts behind Idris (I’ve played with Idris 1 in the past, not yet with Idris 2) and it is great that some form of dependent typing makes its way to the BEAM! :slight_smile:

1 Like

One of the more exciting projects I’ve read about recently. Thanks for sharing!

1 Like