You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
rhiannon morris defdbc74a2 sirdi 5 months ago
.github [ ci ] Set up CI (#5) 12 months ago
src [ version ] bump idris2 version (#13) 7 months ago
.editorconfig [ ci ] Set up CI (#5) 12 months ago
.gitignore initial commit 2 years ago
.idris-version [ version ] bump idris2 version (#16) 5 months ago
LICENSE initial commit 2 years ago
Makefile [ make ] cleaned up makefile 1 year ago [ ci ] Set up CI (#5) 12 months ago
sirdi.json sirdi 5 months ago

idris2-sop : Sums of Products

This is a library about generic representations of algebraic data types as n-ary sums over n-ary products inspired by Haskell's sop-core and generic-sop libraries.

While still very much work in progress, many combinators from sop-core are implemented and ready to be used. Implementations for Generic, an interface for converting data types from and to their generic representations as sums of products, can be derived automatically using elaborator reflection. In addition, implementations for Eq, Ord, DecEq, Semigroup, and Monoid can also be derived automatically by going via a data type's generic representation.

Support for providing access to metadata like constructor and argument names of data types has been added recently, together with the ability to automatically derive implementations for Show.

Motivating Example

With just a single import and after enabling %language ElabReflection, interface implementations can be derived as follows:

module README

import Generics.Derive

%language ElabReflection

record Employee where
  constructor MkEmployee
  name       : String
  age        : Nat
  salary     : Double
  supervisor : Maybe Employee

%runElab derive "Employee" [Generic, Meta, Eq, Ord, Show]

Note: If a data type includes lazy fields, module Data.Lazy should be imported as well when deriving interface implementations.


Most of the exported functions have been properly annotated with doc strings. In addition, there is an extensive - and still growing - tutorial about the core ideas and techniques behind the SOP approach to generic programming.


In order to automatically derive interface implementations, this library makes use of functionality provided by the idris2-elab-util package.

Idris2 Version

Starting from Idris2 version 0.5.1, tagged releases of the same minor version number (e.g. 0.5.x) will be made available, while the main branch keeps following the Idris2 main branch.

The latest commit has been built against Idris 2 of version set in the .idris-version file. This file contains a version in the format which git describe --tags gives.


Below is a non-comprehensive list of limitations and caveats of this library.


The totality checker does not consider derived interface implementations for inductive types to be total, since from the conversion to the generic representation it seems not to be able to figure out that the values to be processed are actually getting any smaller.


This library has not yet been optimized in terms of performance. For instance, there have so far been no investigations into the amount of laziness we should support when converting values from and to their generic representations. In contrast do the Haskell version, NP and NS are both strict heterogeneous containers.

Also, generic Eq and Ord implementations might carry out more comparisons than stricly necessary in cases where the result can be decided early on.