||5 months ago|
|.github||12 months ago|
|src||7 months ago|
|.editorconfig||12 months ago|
|.gitignore||2 years ago|
|.idris-version||5 months ago|
|LICENSE||2 years ago|
|Makefile||1 year ago|
|README.md||12 months ago|
|sirdi.json||5 months ago|
idris2-sop : Sums of Products
While still very much work in progress, many combinators from sop-core
are implemented and ready to be used. Implementations for
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
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
With just a single import and after enabling
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
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.
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
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
NS are both strict heterogeneous
Ord implementations might carry out more
comparisons than stricly necessary in cases where the
result can be decided early on.