decidable

Combinators for manipulating dependently-typed predicates.

https://github.com/mstksg/decidable#readme

Version on this page:0.1.5.0
LTS Haskell 14.27:0.1.5.0
Stackage Nightly 2019-09-21:0.2.1.0
Latest on Hackage:0.3.1.1

See all snapshots decidable appears in

BSD-3-Clause licensed by Justin Le
Maintained by [email protected]
This version can be pinned in stack with:decidable-0.1.5.0@sha256:f79f76ff63858257292cf67c75051d95c868c3ad8a54230f1f403349c7955723,1724
Depends on 2 packages(full list with versions):
Used by 1 package in nightly-2019-07-26(full list with versions):

decidable

decidable on Hackage Build Status

This library provides combinators and typeclasses for working and manipulating type-level predicates in Haskell, which are represented as matchable type-level functions k ~> Type from the singletons library. See Data.Type.Predicate for a good starting point, and the documentation for Predicate on how to define predicates.

Changes

Changelog

Version 0.1.5.0

March 6, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.5.0

  • Add allToAny to Data.Type.Predicate.Quantification.
  • Add PPMapV, EqBy, and IsTC to Data.Type.Predicate.Param.
  • Kind-indexed singletons for indices in Data.Type.Universe.

Version 0.1.4.0

October 29, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.4.0

  • Added tripleNegation and negateTwice to Data.Type.Predicate.Logic, for more constructivist principles.
  • Renamed excludedMiddle to complementation.
  • Add TyPP, SearchableTC, searchTC, SelectableTC, selectTC to Data.Type.Predicate.Param, to mirror TyPred and the DecidableTC/ProvableTC interface from Data.Type.Predicate

Version 0.1.3.1

October 26, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.3.1

  • BUGFIX Remove overlapping Auto instances for IsNothing and IsLeft.

Version 0.1.3.0

October 24, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.3.0

  • Added a type and Universe for universe disjunction or summing, :+:, with appropriate Elem and Auto instances.
  • Added Universe instances (and appropriate Elem and Auto instances) for Proxy (the null universe) and Identity.
  • Auto instances for IsNothing and IsLeft.

Version 0.1.2.0

October 14, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.2.0

  • New :.: for universe composition, with Elem and Universe instances, and associated functions for working with them alongside Any, All.
  • Many of the Elem instances and indices in Data.Type.Universe have had their name changed to be more consistent with their role as indices. IsJust is now IJust, IsRight is IRight, Snd is ISnd.
  • Convenience predicates for alternate universes, such as IsJust, IsLeft, IsNothing, etc.
  • NotAll quantifier added alongside None.
  • Many new implications added to Data.Type.Predicate.Quantification, converting not-any and all-not, etc.
  • NotFound p added as a convenience predicate synonym for Not (Found p).
  • Some implications showing the equivalence between Found (InP f) and NotNull f added 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 Refuted and Decision added to Data.Type.Predicate: elimDisproof and mapRefuted.

Version 0.1.1.0

October 12, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.1.0

  • flipDecision, forgetDisproof, forgetProof, isProved, and isDisproved added to Data.Type.Predicate module.
  • ProvableTC, DeccidableTC, proveTC, and decideTC helper functions and constraints
  • Data.Type.Predicate.Auto module, for generating witnesses at compile-time.
  • Instances for injection and projection out of &&& and |||, with some tricks to prevent overlapping instance issues.

Version 0.1.0.0

October 10, 2018

https://github.com/mstksg/decidable/releases/tag/v0.1.0.0

  • Initial release.