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).
- The compiler can check that a function is total, which means that the function won’t crash or go into an infinite loop.
-
Quantitative type theory
- Can be used for:
- Decide which values/types are available at run-time
- Create messaging protocols with linear types
- Can be used for:
-
Referential transparency
- 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 toderiving
in Haskell) - Automate proofs
- Can be used for:
- 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.
- Basic support for separate compilation. Use together with
- 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 theErlang
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
- https://github.com/chrrasmussen/Idris2-Erlang/tree/master/samples — Code samples of how to do interop, concurrency etc.
- https://github.com/chrrasmussen/typedtext.io — A website written mostly in Idris 2. Built on top of Phoenix Framework.
Remaining issues
The biggest remaining issues regarding the Erlang code generator:
- Improve the performance of the generated Erlang code
- Make the Erlang code generator standalone
- Improve IORef/Buffer implementations
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.