This library provides combinators and typeclasses for working and manipulating
type-level predicates in Haskell, which are represented as matchable type-level
k ~> Type from the singletons library. See Data.Type.Predicate
for a good starting point, and the documentation for
Predicate on how to
October 29, 2018
negateTwiceto Data.Type.Predicate.Logic, for more constructivist principles.
selectTCto Data.Type.Predicate.Param, to mirror
ProvableTCinterface from Data.Type.Predicate
October 26, 2018
- BUGFIX Remove overlapping
October 24, 2018
- Added a type and
Universefor universe disjunction or summing,
:+:, with appropriate
Universeinstances (and appropriate
Proxy(the null universe) and
October 14, 2018
:.:for universe composition, with
Universeinstances, and associated functions for working with them alongside
- Many of the
Eleminstances and indices in Data.Type.Universe have had their name changed to be more consistent with their role as indices.
- Convenience predicates for alternate universes, such as
NotAllquantifier added alongside
- Many new implications added to Data.Type.Predicate.Quantification, converting not-any and all-not, etc.
NotFound padded as a convenience predicate synonym for
Not (Found p).
- Some implications showing the equivalence between
Found (InP f)and
NotNull fadded to Data.Type.Predicate.Param.
- Many new deduction rules added to Data.Type.Predicate.Auto. Please see module documentation for a detailed list of new rules and classes in this version.
- Convenient combinators for dealing with
Decisionadded to Data.Type.Predicate:
October 12, 2018
isDisprovedadded to Data.Type.Predicate module.
decideTChelper functions and constraints
- Data.Type.Predicate.Auto module, for generating witnesses at compile-time.
- Instances for injection and projection out of
|||, with some tricks to prevent overlapping instance issues.
October 10, 2018
- Initial release.