# Idris2-Erlang

[![Ubuntu CI](](
[![macOS CI](](
[![Nix CI](](

Erlang code generator for [Idris 2]( Currently this repository includes a full copy of the Idris 2 compiler, but at some point I want to make this repository into a standalone code generator.

Note that this project is still **work in progress**. Feedback and contributions are appreciated!

### About Idris 2

Idris 2 is a purely functional programming language with first class types. The development of Idris 2 is led by [Edwin Brady]( More information about Idris 2 is available at:

- [Idris website](
- [Idris 2 documentation](
- [Idris 2 repository](

## About the Erlang code generator

### Goals

- Make it easy to interoperate with Erlang.
- Type-safe: It should be difficult to accidentally introduce run-time errors, even when doing interop with Erlang.

### Non-goals

- Make the generated Erlang code readable.

### Currently supported functionality

- 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](idris2/libs/erlang/Erlang/Types.idr). [1]
  - Call almost any Erlang function from Idris.
  - Export Idris functions to be called from Erlang code.
  - Includes [decoding functions](idris2/libs/erlang/Erlang/Decode.idr) to safely convert untyped Erlang values to typed Idris values.
- Supports most of the functionality provided by the `base` package. (Currently a few modules are placed in the `Erlang` namespace)

## Basic usage

Create a file called `Main.idr` with the following content:

module Main

main : IO ()
main = putStrLn "Hello Joe"

Run the Idris 2 program via generated Erlang code: `idris2erl --exec main Main.idr`

More code samples:
- [samples](samples) directory — Examples of using the FFI, concurrency etc.
- []( ([Source]( — Website written in Idris 2, running on the Erlang VM.

## Installation

To run the generated Erlang code, [Erlang OTP 21.2]( or newer is recommended.

There are three alternative methods to install Idris 2 with the Erlang code generator:

1. [From Erlang source code](#alternative-1-from-erlang-source-code) — Easiest way to get started. **Note: Idris 2 running on Erlang is currently much slower than running on Chez Scheme**
2. [From Chez Scheme bootstrap](#alternative-2-from-chez-scheme-bootstrap) — Recommended installation method.
3. [Using an existing `idris2` executable](#alternative-3-using-an-existing-idris2-executable) — Recommended if you want to contribute to `Idris2-Erlang`.

The built executable is named `idris2erl`. This is done to avoid clashing with an existing installation of `idris2`. `idris2erl` is configured to use Erlang as the
default code generator.

### Alternative 1: From Erlang source code

This repository contains a [rebar3]( project that can build a standalone Escript executable. The Escript contains the libraries and can be freely moved around. The Erlang run-time needs to be available to run this Escript.

The generated Erlang source files are only included in specific [releases](, and not in the `master` branch.

1. `git clone`
2. `cd Idris2-Erlang`
3. `git checkout v0.2.1-alpha.1`
4. `rebar3 escriptize`

The Escript executable is built to `_build/default/bin/idris2erl`.

### Alternative 2: From Chez Scheme bootstrap

This installation method requires [Chez Scheme]( to be installed.

1. `git clone`
2. `cd Idris2-Erlang/idris2`
3. `make bootstrap SCHEME=chez` (Replace `chez` with the name of your installed version of Chez Scheme)
4. `make install`

This will install the `idris2erl` executable, libraries and support files into `$HOME/.idris2erl`. For easy access, add `$HOME/.idris2erl/bin` directory to your `$PATH`.

### Alternative 3: Using an existing `idris2` executable

This installation method requires [Chez Scheme]( to be installed, and that you have `idris2` available in `$PATH`. To install the official version of Idris 2, see [Idris 2's installation instructions](

1. `git clone`
2. `cd Idris2-Erlang/idris2`
3. `make all`
4. `make install`

This will install the `idris2erl` executable, libraries and support files into `$HOME/.idris2erl`. For easy access, add `$HOME/.idris2erl/bin` directory to your `$PATH`.

## Editor support

Idris 2 supports interactive editing. See [Idris 2's download page]( for a list of supported editors.

In my experience, the Idris 1 extensions for [Visual Studio Code]( and [Atom]( mostly works for Idris 2. After installing the extension, you need to change location of the Idris executable to point to `idris2erl`.

## Documentation

### Erlang code generator

The Idris 2 libraries tries to include documentation for its functions and data types. The documentation can be accessed using the `:doc` command in the Idris 2 REPL.

- [Overview of data types that have a mapping between Idris 2 and Erlang](docs/
- [Codegen-specific directives](docs/
- [Intermediate representations](docs/

- [Hello world](samples/1-HelloWorld)
- [Foreign function interface (FFI)](samples/2-FFI)
- [Decoding Erlang values](samples/3-Decoding)
- [Concurrency](samples/4-Concurrency)
- [Library](samples/5-Library)

### Learning Idris 2

- [A Crash Course in Idris 2](
  - This tutorial assumes some existing experience with functional programming.
- [Type-Driven Development with Idris by Edwin Brady](
  - The book was written with Idris 1 in mind, but the knowledge is transferable to Idris 2. [This document]( describes what changes are necessary to run the code samples from the book in Idris 2.
  - This book is how I got started with Idris :-)
- [The Idris 2 lists some talks given by Edwin Brady](
  - These videos are mainly presenting what's new in Idris 2, but they may provide motivation for why Idris 2 is an interesting language.

## Community

The [Idris website]( contains links to where you can find the Idris community.

## License

The Idris 2 compiler is released under the [3-clause BSD license](idris2/LICENSE).

The Erlang code generator is derived from the Idris 2 compiler and is released under the [3-clause BSD license](LICENSE).



[1] `bitstring` is not supported as a separate data type. Some data types, such as tuples and functions, include a size/arity in their names: These data types are currently limited to a maximum size/arity of `8`.