Extending Idris using Elaborator Reflection

Idris provides a mechanism to modify the language without having to recompile Idris itself. We can think of this in terms of metaprogramming or domain specific languages or just building in new capabilities.

In order to extend the language we need to know something about how Idris is complied. On this page we try to limit this explanation to only what we need to customise the elaboration. For more details of the compiler see [1] and for customising the elaboration process see [2].

Here is a diagram of the multistage process at the top level when Idris code gets compiled:

idris top level

TT is a core language which is syntactically very simple but this makes it easy for computers to process but very verbose and hard for humans to read.

This elaboration is done by a logic language (proof tactics) like LTac in Coq. Here we use the word 'tactics' to refer to these elaboration tactics - not to be confused with the old tactics mechanism.

compare to proof assistant

This gives the opportunity to allow the primitives of the elaboration mechanism to be exposed to metaprograms.

During elaboration TT (Raw) structure contains:

Type checker:

elaboration overview

 

elab monad

Is this old tactics:

tactic

As already mentioned the TT core language is kept syntactically very simple. Part of the reason for this is that its correctness is already well proven using logic. For instance, here are the binders in TT with corresponding code and logic type introduction rules:

TT binders

   

AsPat

Code to elaborate pattern variables.

 code

Clause

Code to elaborate clauses.

 code

Data

Code to elaborate data structures.

 code

Implementation

Code to elaborate instances.

 code

Interface

Code to elaborate interfaces.

 code

Provider

Code to elaborate type providers.

 code

Quasiquote

Code to elaborate quasiquotations.

 code

Record

Code to elaborate records.

 code

Rewrite

Code to elaborate rewrite rules.

 code

RunElab

Code to run the elaborator process.

 code

Term

Code to elaborate terms.

 code

Transform

Transformations for elaborate terms.

 code

Type

Code to elaborate types.

 code

Utils

Elaborator utilities.

 code

Value

Code to elaborate values.

 code

 

[1] Edwin Brady’s 2013 paper

[2] Practical Reflection and Metaprogramming for Dependent Types David Christiansen

[3] Unification Algorithms

metadata block
see also:
Correspondence about this page

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.