|
1 year ago | |
---|---|---|
.github | 2 years ago | |
src | 1 year ago | |
.editorconfig | 2 years ago | |
.gitignore | 3 years ago | |
.idris-version | 1 year ago | |
LICENSE | 3 years ago | |
Makefile | 2 years ago | |
README.md | 2 years ago | |
sirdi.json | 1 year ago |
README.md
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.
Documentation
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.
Prerequisites
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.
Limitations
Below is a non-comprehensive list of limitations and caveats of this library.
Totality
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.
Performance
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.