eliminators

Dependently typed elimination functions using singletons

BSD-3-Clause licensed by Ryan Scott

Maintained by Ryan Scott

This version can be pinned in stack with:eliminators-0.7@sha256:9689531d590aa2ee489011a1acdf5f42269d343783b741e9440d5b3f0b39e8ae,2727

Depends on 7 packages(full list with versions):

`eliminators`

This library provides eliminators for inductive data types, leveraging the power of the singletons library to allow dependently typed elimination.

Require singletons-2.7 and GHC 8.10.
Add experimental support for generating type-level eliminators through the deriveTypeElim and deriveTypeElimNamed functions.
Add eliminators for All, Any, Arg, Const, Down, Dual, First, Identity, Last, Max, Min, Option, Product, Sum, and WrappedMonoid.

Migrate the old elimNat from Data.Eliminator (which worked over the Nat from GHC.TypeNats) to Data.Eliminator.TypeNats. There elimNat that now lives in Data.Eliminator is for an unrelated Nat data type from the singleton-nats package (which is a proper, inductively defined, Peano natural number type).

Introduce the Data.Eliminator.TH module, which provides functionality for generating eliminator functions using Template Haskell. Currently, only simple algebraic data types that do not use polymorphic recursion are supported.
All eliminators now use predicates with (~>).