Idris2 Go

Idris2 Go is a library for generating go programs and an Idris2 compiler backend for generating go programs from Idris2 source code.

This tool is for experimental use only, relying on it in production systems is not advised. While some Idris2 programs might work with this tool, there are some features missing, which can make the generated programs unusable (mainly on non-Linux OS-es) or slow (compared to other backends).

Installation

The easiest way to install idris2-go is to use idris2-pack:

pack install-app idris2-go

Build

The provided Makefile also assumes the presense of idris2-pack on your system.

Currently it is developed on linux, using (almost) latest Idris2 and latest go (version 1.20.x). If something is not working for you, then please consider to update your versions.

For the impatient you can check the below commands to build test runner and all tests using idris2-go:

make clean
make build

make install
make test

make install-lib
IDRIS2=idris2-go make test-lib

Current state and ideas

Go code generator

• Language features
  • Packages, imports
  • Variables and constants
  • Functions
  • Structs, arrays, slices and maps
  • Flow control
  • Methods
  • Interfaces
  • Generics
  • Concurrency
• Generator
  • AST
  • Combinators
  • Code printer
  • Tour of Go tests
  • Comment handling (it is incomplete, and alreay opinionated)

Compiler

• Whole program compiler
• Expression compiler for REPL
• Compile test lib, and run tests using it
• Tail call optimozation from Idris2 ES
• Compiles itself (about 2x slower than compiling with chez backend, and it uses about 10GB ram)
• Basic FFI support
• Specialize constructor cases
• Reduce function literal calls if possible
• Windows support
• Mac support
• More mature FFI parsing and type support
• Implement missing FFI methods for libraries and Idris2 compiler
• Persistent data structures for list
• Performance tests and tuning

Project

• Install via pack
• Build / Test pipeline