Introduction

When programming one core activity is to declare suitable types to model and shape the data that our program will be working with. One common feature that one might want to use is to automatically derive properties from the type definition. Such systems exist in other programming languages such as Haskell with deriving or Rust with derive. They offer different levels of flexibility and obey different rules but they aim to solve the same problem: Alleviate the need to write (usually obvious) code when the computer can do it for you.

Current status

Idris2 has no such facility but it has elaborator reflection (this points to the documentation for Idris1 because the one for Idris2 has not been written yet), which allows you to hook into Idris' elaborator for different purposes. One of them is to generate new instances such as Eq and DecEq.

Proposed solution

However we believe there is a better way to go about solving this particular problem of synthesising instances. Previous work about levitation (https://jmchapman.io/papers/levitation.pdf, http://itu.dk/people/asal/pubs/msc-thesis-report.pdf) indicate that it is possible to define data types in terms of data types, we call the data type that describe data types Desc. given a type declaration, the compiler could synthesize its Desc and use it to derive any interface that is already valid on Desc to the type declared.

Additionally, having the compiler have a native Desc internal representation would allow:

• To move all type meta-programming outside elaborator reflection and into the language. Users could define functions from Desc to Desc in order to explain how to convert from one type definition to another.
• Implementing optimisation on types by providing a bijection between a user-defined type and a specially optimised type (for example a user-defined Nat and the Nat type from the prelude)
• Desc could be augmented to be ornaments https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/journal-2013-catorn-jfp/paper.pdf Which would provide ways of reusing function implementations for indexed version of types, implement some form of row-polymorphism and some form of versionning of type definitions at the level of the language, rather than at the meta-level.

Known limitations

Previous work with Idris1 has shown that using levitated types is slow. But there is additional work to attempt, namely, the compiler could simply learn from the synthesized Desc and implement every interface using known safe coercions from the Desc to the original type. This idea has proven to be workable with Haskell's deriving via.

Levitation has no notion of quantities, and as such it would only be able to use it on types which have unrestricted fields, linear and erased fields would be disallowed. This is something that could maybe be fixed using quantitative containers but as far as we know this is still a work in progress.