Custom backend cookbook
This document addresses the details on how to implement a custom code generation backend for the Idris compiler.
This part has no insights about how to implement the dependently typed bits. For that part of the compiler Edwin Brady gave lectures at SPLV20 which are available online.
The architecture of the Idris2 compiler makes it easy to implement a custom code generation back-end.
The way to extend Idris with new back-ends is to use it as a library.
The module Idris.Driver
exports the function mainWithCodegens
,
that takes a list of (String, Codegen)
, starting idris with these codegens
in addition to the built-in ones.
The first codegen in the list will be set as the default codegen.
Anyone who is interested in implementing a custom back-end needs to answer the following questions:
Which Intermediate Representation (IR) should be consumed by the custom back-end?
How to represent primitive values defined by the
Core.TT.Constant
type?How to represent Algebraic Data Types?
How to implement special values?
How to implement primitive operations?
How to compile IR expressions?
How to compile Definitions?
How to implement Foreign Function Interface?
How to compile modules?
How to embed code snippets?
What should the runtime system support?
First of all, we should know that Idris2 is not an optimizing compiler. Currently its focus is only to compile dependently typed functional code in a timely manner. Its main purpose is to check if the given program is correct in a dependently typed setting and generate code in form of a lambda-calculus like IR where higher-order functions are present. Idris has 3 intermediate representations for code generation. At every level we get a simpler representation, closer to machine code, but it should be stressed that all the aggressive code optimizations should happen in the custom back-ends. The quality and readability of the generated back-end code is on the shoulders of the implementor of the back-end. Idris erases type information, in the IRs as it compiles to scheme by default, and there is no need to keep the type information around. With this in mind let’s answer the questions above.
The architecture of an Idris back-end
Idris compiles its dependently typed front-end language into a representation
which is called Compile.TT.Term
.
This data type has a few constructors and it represents a dependently typed
term.
This Term
is transformed to Core.CompileExpr.CExp
which has more
constructors than Term
and it is a very similar construct to a lambda
calculus with let bindings, structured and tagged data representation,
primitive operations, external operations, and case expressions.
The CExp
is closer in the compiling process to code generation.
The custom code generation back-end gets
a context of definitions,
a template directory and an output directory,
a Core.TT.ClosedTerm
to compile and a path to an output file.
compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String)
-> ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term file = ?
The ClosedTerm
is a special Term
where the list of the unbound
variables is empty.
This technicality is not important for the code generation of the custom
back-end as the back-end needs to call the getCompileData
function
which produces the Compiler.Common.CompileData
record.
The CompileData
contains:
A main expression that will be the entry point for the program in
CExp
A list of
Core.CompileExpr.NamedDef
A list of lambda-lifted definitions
Compiler.LambdaLift.LiftedDef
A list of
Compiler.ANF.ANFDef
A list of
Compiler.VMCode.VMDef
definitions
These lists contain:
Functions
Top-level data definitions
Runtime crashes which represent unfilled holes, explicit calls by the user to
idris_crash
, and unreachable branches in case treesForeign call constructs
The job of the custom code generation back-end is to transform one of the phase
encoded definitions (NamedDef
, LiftedDef
, CExp
, ANF
, or VM
)
into the intermediate representation of the code generator.
It can then run optimizations and generate some form of executable.
In summary, the code generator has to understand how to represent tagged data
and function applications (even if the function application is partial), how
to handle let expressions, how to implement and invoke primitive operations,
how to handle Erased
arguments, and how to do runtime crashes.
The implementor of the custom back-end should pick the closest Idris IR which fits to the abstraction of the technology that is aimed to compile to. The implementor should also consider how to transform the simple main expression which is represented in CExp. As Idris does not focus on memory management and threading. The custom back-end should model these concepts for the program that is compiled. One possible approach is to target a fairly high level language and reuse as much as possible from it for the custom back-end. Another possibility is to implement a runtime that is capable of handling memory management and threading.
Which Intermediate Representation (IR) should be consumed by the custom back-end?
Now lets turn our attention to the different intermediate representations (IRs)
that Idris provides.
When the getCompileData
function is invoked with the UsePhase
parameter
it will produce a CompileData
record, which will contain lists of top-level
definitions that needs to be compiled. These are:
NamedDef
LiftedDef
ANFDef
VMDef
The question to answer here is: Which one should be picked? Which one fits to the custom back-end?
How to represent primitive values defined by the Core.TT.Constant
type?
After one selects the IR to be used during code generation, the next question to answer is how primitive types should be represented in the back-end. Idris has the following primitive types:
Int
Integer
(arbitrary precision)Bits(8/16/32/64)
Char
String
Double
WorldVal
(token for IO computations)
And as Idris allows pattern matching on types all the primitive types have their primitive counterpart for describing a type:
IntType
IntegerType
Bits(8/16/32/64)Type
StringType
CharType
DoubleType
WorldType
The representation of these primitive types should be a well-thought out design decision as it affects many parts of the code generation, such as conversion from the back-end values when FFI is involved, big part of the data during the runtime is represented in these forms. Representation of primitive types affect the possible optimisation techniques, and they also affect the memory management and garbage collection.
There are two special primitive types: String and World.
String
As its name suggest this type represent a string of characters. As mentioned in Primitive FFI Types, Strings are encoded in UTF-8.
It is not always clear who is responsible for freeing up a String
created by
a component other than the Idris runtime. Strings created in Idris will
always have value, unlike possible String representation of the host technology,
where for example NULL pointer can be a value, which can not happen on the Idris side.
This creates constraints on the possible representations of the Strings in the
custom back-end and diverging from the Idris representation is not a good idea.
The best approach here is to build a conversion layer between the string
representation of the custom back-end and the runtime.
World
In pure functional programming, causality needs to be represented whenever we want to maintain the order in which subexpressions are executed. In Idris a token is used to chain IO function calls. This is an abstract notion about the state of the world. For example this information could be the information that the runtime needs for bookkeeping of the running program.
The WorldVal
value in Idris programs is accessed via the primIO
construction which leads us to the PrimIO
module.
Let’s see the relevant snippets:
data IORes : Type -> Type where
MkIORes : (result : a) -> (1 x : %World) -> IORes a
fromPrim : (1 fn : (1 x : %World) -> IORes a) -> IO a
fromPrim op = MkIO op
primIO : HasIO io => (1 fn : (1 x : %World) -> IORes a) -> io a
primIO op = liftIO (fromPrim op)
The world value is referenced as %World
in Idris.
It is created by the runtime when the program starts.
Its content is changed by the custom runtime.
More precisely, the World is created when the WorldVal
is evaluated during
the execution of the program.
This can happen when the program gets initialized or when an unsafePerformIO
function is executed.
How to represent Algebraic Data Types?
In Idris there are two different ways to define a data type: tagged unions are
introduced using the data
keyword while structs are declared via the
record
keyword.
Declaring a record
amounts to defining a named collection of fields.
Let’s see examples for both:
data Either a b
= Left a
| Right b
record Pair a b
constructor MkPair
fst : a
snd : b
Idris offers not only algebraic data types but also indexed families. These
are tagged union where different constructors may have different return types.
Here is Vect
an example of a data type which is an indexed family
corresponding to a linked-list whose length is known at compile time.
It has one index (of type Nat
) representing the length of the list (the
value of this index is therefore different for the []
and (::)
constructors) and a parameter (of type Type
) corresponding to the type
of values stored in the list.
data Vect : (size : Nat) -> Type -> Type where
Nil : Vect 0 a -- empty list: size is 0
(::) : a -> Vect n a -> Vect (1 + n) a -- extending a list of size n: size is 1+n
Both data and record are compiled to constructors in the intermediate
representations. Two examples of such Constructors are
Core.CompileExpr.CExp.CCon
and Core.CompileExpr.CDef.MkCon
.
Compiling the Either
data type will produce three constructor definitions
in the IR:
One for the
Either
type itself, with the arity of two. Arity tells how many parameters of the constructor should have. Two is reasonable in this case as the original IdrisEither
type has two parameters.One for the
Left
constructor with arity of three. Three may be surprising, as the constructor only has one argument in Idris, but we should keep in mind the type parameters for the data type too.One for the
Right
constructor with arity of three.
In the IR constructors have unique names. For efficiency reasons,
Idris assigns a unique integer tag to each data constructors so that constructor
matching is reduced to comparisons of integers instead of strings.
In the Either
example above Left
gets tag 0 and Right
gets tag 1.
Constructors can be considered structured information: a name
together with parameters.
The custom back-end needs to decide how to represent such data.
For example using Dict
in Python, JSON
in JavaScript, etc.
The most important aspect to consider is that these structured values
are heap related values, which should be created and stored dynamically.
If there is an easy way to map in the host technology, the memory management
for these values could be inherited. If not, then the host technology is
responsible for implementing an appropriate memory management.
For example RefC
is a C backend that implements its own memory management
based on reference counting.
How to implement special values?
Apart from the data constructors there are two special kind of values present
in the Idris IRs: type constructors and Erased
.
Type constructors
Type and data constructors that are not relevant for the program’s runtime behaviour may be used at compile butand will be erased from the intermediate representation.
However some type constructors need to be kept around even at runtime because pattern matching on types is allowed in Idris:
notId : {a : Type} -> a -> a
notId {a=Int} x = x + 1
notId x = x
Here we can pattern match on a
and ensure that notId
behaves differently
on Int
than all the other types.
This will generate an IR that will contain a Case
expression with two
branches:
one Alt
matching on the Int
type constructor
and a default for the non-Int
matching part of the notId
function.
This is not that special: Type
is a bit like an infinite data type that
contains all of the types a user may ever declare or use.
This can be handled in the back-end and host language using the same mechanisms
that were mobilised to deal with data constructors.
The reason for using the same approach is that in dependently typed languages,
the same language is used to form both type and value level expressions.
Compilation of type level terms will be the same as that of value level terms.
This is one of the things that make dependently typed abstraction elegant.
Erased
The other kind of special value is Erased
.
This is generated by the Idris compiler and part of the IR if the original value
is only needed during the type elaboration process. For example:
data Subset : (type : Type)
-> (pred : type -> Type)
-> Type
where
Element : (value : type)
-> (0 prf : pred value)
-> Subset type pred
Because prf
has quantity 0
, it is guaranteed to be erased during
compilation and thus not present at runtime.
Therefore prf
will be represented as Erased
in the IR.
The custom back-end needs to represent this value too as any other data value,
as it could occur in place of normal values.
The simplest approach is to implement it as a special data constructor and let
the host technology provided optimizations take care of its removal.
How to implement primitive operations?
Primitive operations are defined in the module Core.TT.PrimFn
.
The constructors of this data type represent the primitive operations that
the custom back-end needs to implement.
These primitive operations can be grouped as:
Arithmetic operations (
Add
,Sub
,Mul
,Div
,Mod
,Neg
)Bit operations (
ShiftL
,ShiftR
,BAnd
,BOr
,BXor
)Comparison operations (
LT
,LTE
,EQ
,GTE
,GT
)String operations (
Length
,Head
,Tail
,Index
,Cons
,Append
,Reverse
,Substr
)Double precision floating point operations (
Exp
,Log
,Sin
,Cos
,Tan
,ASin
,ACos
,ATan
,Sqrt
,Floor
,Ceiling
)Casting of numeric and string values
An unsafe cast operation
BelieveMe
A
Crash
operation taking a type and a string and creating a value at that type by raising an error.
BelieveMe
The primitive believe_me
is an unsafe cast that allows users to bypass the
typechecker when they know something to be true even though it cannot be proven.
For instance, assuming that Idris’ primitives are correctly implemented, it
should be true that if a boolean equality test on two Int
i
and j
returns True
then i
and j
are equal.
Such a theorem can be implemented by using believe_me
to cast Refl
(the constructor for proofs of a propositional equality) from i === i
to
i === j
. In this case, it should be safe to implement.
Boxing
Idris assumes that the back-end representation of the data is not strongly typed and that all the data type have the same kind of representation. This could introduce a constraint on the representation of the primitives and constructor represented data types. One possible solution is that the custom back-end should represent primitive data types the same way it does constructors, using special tags. This is called boxing.
Official backends represent primitive data types as boxed ones.
RefC: Boxes the primitives, which makes them easy to put on the heap.
Scheme: Prints the values that are a
Constant
as Scheme literals.
How to compile top-level definitions?
As mentioned earlier, Idris has 4 different IRs that are available in
the CompileData
record: Named
, LambdaLifted
, ANF
, and VMDef
.
When assembling the CompileData
we have to tell the Idris compiler which
level we are interested in.
The CompileData
contains lists of definitions that can be considered as top
level definitions that the custom back-end need to generate functions for.
There are four types of top-level definitions that the code generation back-end needs to support:
Function
Constructor
Foreign call
Error
Function contains a lambda calculus like expression.
Constructor represents a data or a type constructor, and it should be implemented as a function creating the corresponding data structure in the custom back-end.
A top-level foreign call defines an entry point for calling functions implemented outside the Idris program under compilation. The Foreign construction contains a list of Strings which are the snippets defined by the programmer, the type of the arguments and the return type of the foreign function. The custom back-end should generate a wrapper function. More on this on How to implement the Foreign Function Interface?
A top-level error definition represents holes in Idris programs, uses of
idris_crash
, or unreachable branches in a case tree.
Users may want to execute incomplete programs for testing purposes which is
fine as long as we never actually need the value of any of the holes.
Library writers may want to raise an exception if an unrecoverable error has
happened.
Finally, Idris compiles the unreachable branches of a case tree to runtime
error as it is dead code anyway.
How to compile IR expressions?
The custom back-end should decide which intermediate representation is used as a starting point. The result of the transformation should be expressions and functions of the host technology.
Definitions in ANF
and Lifted
are represented as a tree like expression,
where control flow is based on the Let
and Case
expressions.
Case expressions
There are two types of case expressions,
one for matching and branching on primitive values such as Int
,
and the second one is matching and branching on constructor values.
The two types of case expressions will have two different representation for
alternatives of the cases. These are ConstCase
(for matching on constant
values) and ConCase
(for matching on constructors).
Matching on constructors can be implemented as matching on their tags or, less efficiently, as matching on the name of the constructor. In both cases a match should bind the values of the constructor’s arguments to variables in the body of the matching branch. This can be implemented in various ways depending on the host technology: switch expressions, case with pattern matching, or if-then-else chains.
When pattern matching binds variables, the number of arguments can be different
from the arity of the constructor defined in top-level definitions and in
GlobalDef
. This is because all the arguments are kept around at typechecking
time, but the code generator for the case tree removes the ones which are marked
as erased. The code generator of the custom back-end also needs to remove the
erased arguments in the constructor implementation.
In GlobalDef
, eraseArg
contains this information, which can be used to
extract the number of arguments which needs to be kept around.
Creating values
Values can be created in two ways.
If the value is a primitive value, it will be handed to the back-end as
a PrimVal
. It should be compiled to a constant in the host language
following the design decisions made in
the ‘How to represent primitive values?’ section.
If it is a structured value (i.e. a Con
) it should be compiled to a function
in the host language which creates a dynamic value. Design decisions made for
‘How to represent constructor values?’ is going to have effect here.
Function calls
There are four types of function calls:
- Saturated function calls (all the arguments are there)
- Under-applied function calls (some arguments are missing)
- Primitive function calls (necessarily saturated, PrimFn
constructor)
- Foreign Function calls (referred to by its name)
The ANF
and Lifted
intermediate representations support under-applied
function calls (using the UnderApp
constructor in both IR).
The custom back-end needs to support partial application of functions and
creating closures in the host technology.
This is not a problem with back-ends like Scheme where we get the partial
application of a function for free.
But if the host language does not have this tool in its toolbox, the custom
back-end needs to simulate closures.
One possible solution is to manufacture a closure as a special object storing
the function and the values it is currently applied to and wait until all the
necessary arguments have been received before evaluating it.
The same approach is needed if the VMCode
IR was chosen for code generation.
Let bindings
Both the ANF
and Lifted
intermediate representations have a
Let
construct that lets users assign values to local variables.
These two IRs differ in their representation of bound variables.
Lifted
is a type family indexed by the List Name
of local variables
in scope. A variable is represented using LLocal
, a constructor that
stores a Nat
together with a proof that it points to a valid name in
the local scope.
ANF
is a lower level representation where this kind of guarantees are not
present anymore. A local variable is represented using the AV
constructor
which stores an AVar
whose definition we include below.
The ALocal
constructor stores an Int
that corresponds to the Nat
we would have seen in Lifted
.
The ANull
constructor refers to an erased variable and its representation
in the host language will depend on the design choices made in
the ‘How to represent Erased
values’ section.
VMDef specificities
VMDef
is meant to be the closest IR to machine code.
In VMDef
, all the definitions have been compiled to instructions for a small
virtual machine with registers and closures.
Instead of Let
expressions, there only are ASSIGN
statements
at this level.
Instead of Case
expressions binding variables when they successfully match
on a data constructor, CASE
picks a branch based on the constructor itself.
An extra operation called PROJECT
is introduced to explicitly extract a
constructor’s argument based on their position.
There are no App
or UnderApp
. Both are replaced by APPLY
which
applies only one value and creates a closure from the application. For erased
values the operation NULL
assigns an empty/null value for the register.
How to implement the Foreign Function Interface?
The Foreign Function Interface (FFI) plays a big role in running Idris programs.
The primitive operations which are mentioned above are functions for
manipulating values and those functions aren’t meant for complex interaction
with the runtime system.
Many of the primitive types can be thought of as abstract types provided via
external
and foreign functions to manipulate them.
The responsibility of the custom back-end and the host technology is to represent these computations the operationally correct way. The design decisions with respect to representing primitive types in the host technology will inevitably have effects on the design of the FFI.
Foreign Types
Originally Idris had an official back-end implementation in C. Even though
this has changed, the names in the types for the FFI kept their C prefix.
The Core.CompileExpr.CFType
contains the following definitions, many of
them one-to-one mapping from the corresponding primitive type, but some of
them needs explanation.
The foreign types are:
CFUnit
CFInt
CFUnsigned(8/16/32/64)
CFString
CFDouble
CFChar
CFFun
of typeCFType -> CFType -> CFType
Callbacks can be registered in the host technology via parameters that have CFFun type. The back-end should be able to handle functions that are defined in Idris side and compiled to the host technology. If the custom back-end supports higher order functions then it should be used to implement the support for this kind of FFI type.CFIORes
of typeCFType -> CFType
AnyPrimIO
defined computation will have this extra layer. Pure functions shouldn’t have any observable IO effect on the program state in the host technology implemented runtime. NOTE:IORes
is also used when callback functions are registered in the host technology.CFWorld
Represents the current state of the world. This should refer to a token that is passed around between function calls. The implementation of the World value should contain back-end specific values and information about the state of the Idris runtime.CFStruct
of typeString -> List (String, CFType) -> CFType
is the foreign type associated with theSystem.FFI.Struct
. It represents a C like structure in the custom back-end.prim__getField
andprim__setField
primitives should be implemented to support this CFType.CFUser
of typeName -> List CFType -> CFType
Types defined with [external] are represented withCFUser
. For exampledata MyType : Type where [external]
will be represented asCFUser Module.MyType []
CFBuffer
Foreign type defined forData.Buffer
. Although this is an external type, Idris builds on a random access buffer.CFPtr
ThePtr t
andAnyPtr
are compiled toCFPtr
Any complex structured data that can not be represented as a simple primitive can use this CFPtr to keep track where the value is used. In IdrisPtr t
is defined as external type.CFGCPtr
TheGCPtr t
andGCAnyPtr
are compiled toCFGCPtr
.GCPtr
is inferred from a Ptr value calling theonCollect
function and has a special property. TheonCollect
attaches a finalizer for the pointer which should run when the pointer is freed.
Examples
Let’s step back and look into how this is represented at the Idris source level.
The simplest form of a definition involving the FFI a function definition with
a %foreign
pragma. The pragma is passed a list of strings corresponding to
a mapping from backends to names for the foreign calls. For instance:
this function should be translated by the C back end as a call to the add
function defined in the smallc.c
file. In the FFI, Int
is translated to
CFInt
. The back-end assumes that the data representation specified in the
library file correspond to that of normal Idris values.
We can also define external
types like in the following examples:
Here ThreadID
is defined as an external type and this type will be
represented as CFUser "ThreadID" []
internally. The value which is
created by the scheme runtime will be considered as a black box.
The type of prim__fork
, once translated as a foreign type, is
[%World -> IORes Unit, %World] -> IORes Main.ThreadID
Here we see that the %World
is added to the IO computations.
The %World
parameter is always the last in the argument list.
For the FFI functions, the type information and the user defined string can
be found in the top-level definitions.
The custom back-end should use the definitions to generate wrapper code,
which should convert the types that are described by the CFType
to the
types that the function in the %foreign
directive needs..
How to compile modules?
The Idris compiler generates intermediate files for modules, the content of
the files are neither part of Lifted
, ANF
, nor VMCode
.
Because of this, when the compilation pipeline enters the stage of code
generation, all the information will be in one instance of the CompileData
record and the custom code generator back-end can process them as it would
see the whole program.
The custom back-end has the option to introduce some hierarchy for the functions in different namespaces and organize some module structure to let the host technology process the bits and pieces in different sized chunks. However, this feature is not in the scope of the Idris compiler.
It is worth noting that modules can be mutually recursive in Idris. So a direct compilation of Idris modules to modules in the host language may be unsuccessful.
How to embed code snippets?
A possible motivation for implementing a custom back-end for Idris is to generate code that is meant to be used in a larger project. This project may be bound to another language that has many useful librarie but could benefit from relying on Idris’ strong type system in places.
When writing a code generator for this purpose, the interoperability of the host technology and Idris based on the Foreign Interface can be inconvenient. In this situation, the need to embed code of the host technology arises naturally. Elaboration can be an answer for that.
Elaboration is a typechecking time code generation technique.
It relies on the Elab
monad to write scripts that can interact with the
typechecking machinery to generate Idris code in Core.TT
.
When code snippets need to be embedded a custom library should be provided
with the custom back-end to turn the valid code snippets into their
representation in Core.TT
.
What should the runtime system support?
As a summary, a custom back-end for the Idris compiler should create an environment in the host technology that is able to run Idris programs. As Idris is part of the family of functional programming languages, its computation model is based on graph reduction. Programs represented as simple graphs in the memory are based on the closure creation mechanism during evaluation. Closure creation exist even on the lowest levels of IRs. For that reason any runtime in any host technology needs to support some kind of representation of closures and be able to store them on the heap, thus the responsibility of memory management falls on the lap of the implementor of the custom back-end. If the host technology has memory management, the problem is not difficult. It is also likely that storing closures can be easily implemented via the tools of the host technology.
Although it is not clear how much functionality a back-end should support. Tools from the Scheme back-end are brought into the Idris world via external types and primitive operations around them. This is a good practice and gives the community the ability to focus on the implementation of a quick compiler for a dependently typed language. One of these hidden features is the concurrency primitives. These are part of the different libraries that could be part of the compiler or part of the contribution package. If the threading model is different for the host technology that the Idris default back-end inherits currently from the Scheme technology it could be a bigger piece of work.
IO in Idris is implemented using an abstract %World
value, which serves as token for
functions that operate interactively with the World through simple calls to the
underlying runtime system. The entry point of the program is the main function, which
has the type of the IO unit, such as main : IO ()
. This means that every
program which runs, starts its part of some IO computation. Under the hood this is
implemented via the creation of the %World
abstract value, and invoking the main
function, which is compiled to pass the abstract %World value for IO related
foreign or external operations.
There is an operation called unsafePerformIO
in the PrimIO
module.
The type signature of unsafePerformIO
tells us that it is capable of
evaluating an IO
computation in a pure context.
Under the hood it is run in exactly the same way the main
function is.
It manufactures a fresh %World
token and passes it to the IO
computations.
This leads to a design decision: How to
represent the state of the World, and how to
represent the world that is instantiated for the sake of the unsafePerformIO
operation via the
unsafeCreateWorld
? Both the mechanisms of main
and unsafeCreateWorld
use the %MkWorld
constructor, which will be compiled to WorldVal
and
its type to WorldType
, which means the implementation of the runtime
is responsible for creating the abstraction around the World. Implementation of an
abstract World value could be based on a singleton pattern, where we can have
just one world, or we could have more than one world, resulting in parallel
universes for unsafePerformIO
.