constraints
Constraint manipulation
http://github.com/ekmett/constraints/
Version on this page: | 0.13 |
LTS Haskell 22.37: | 0.14.2@rev:1 |
Stackage Nightly 2024-10-07: | 0.14.2@rev:1 |
Latest on Hackage: | 0.14.2@rev:1 |
constraints-0.13@sha256:d341eb4adbf712f928706928d23a173fb3d0976f0dfaf6a274958975d5fc9e75,2338
Module documentation for 0.13
Changes
0.13 [2021.02.17]
-
Data.Constraint.Symbol
now reexports theGHC.TypeLits.AppendSymbol
type family from recent versions ofbase
(or, on old versions ofbase
, it defines a backwards-compatibile version ofAppendSymbol
). The existing(++)
type family forData.Constraint.Symbol
is now a synonym forAppendSymbol
.This is technically a breaking change, as
(++)
was previously defined like so:type family (++) :: Symbol -> Symbol -> Symbol
This meant that
(++)
could be partially applied. However, for compatibility with the way thatAppendSymbol
is defined,(++)
is now defined like so:type m ++ n = AppendSymbol m n
As a result,
(++)
can no longer be partially applied. -
Make the
(++)
type family inData.Constraint.Symbol
beinfixr 5
. -
Add
implied :: (a => b) -> (a :- b)
toData.Constraint
, which converts a quantified constraint into an entailment. This is only available when compiled with GHC 8.6 or later.
0.12 [2020.02.03]
-
Relax the type signature for
divideTimes
:-dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c) +dividesTimes :: Divides a b :- Divides a (b * c)
-
Simplify the type signature of
dividesDef
:-dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ b) +dividesDef :: forall a b. Divides a b :- (Mod b a ~ 0)
The original type of
diviesDef
can be (partially) recovered by defining it in terms of the newdividesDef
:dividesDef' :: forall a b. (1 <= a, Divides a b) :- ((a * Div b a) ~ b) dividesDef' = Sub $ case (dividesDef @a @b, euclideanNat @a @b) of (Sub Dict, Sub Dict) -> Dict
0.11.2 [2019.09.06]
- Depend on the
type-equality
compatibility library so that(:~~:)
may be used when compiling this library with GHC 8.0. This avoids having to redefine(:~~:)
directly in the internals ofconstraints
itself.
0.11.1 [2019.08.27]
- Make
Data.Constraint.Deferrable.UnsatisfiedConstraint
a newtype.
0.11 [2019.05.10]
- Introduce a
HasDict
type class for types that witness evidence of constraints, such asDict
,(:-)
,Coercion
,(:~:)
,(:~~:)
, andTypeRep
. - Generalize the types of
withDict
and(\\)
to be polymorphic over anyHasDict
instance. - Add
type (⊢) = (:-)
. - Fix unsafe mistakes in the statements of
dividesDef
andtimesDiv
inData.Constraint.Nat
. - Make the implementations of
Min
andMax
reduce on more inputs inData.Constraint.Nat
. - Add
minusNat
andminusZero
functions toData.Constraint.Nat
. - Support
hashable-1.3.*
andsemigroups-0.19.*
.
0.10.1 [2018.07.02]
- Allow building with GHC 8.6.
- Add three axioms about
(+)
and(-)
toData.Constraint.Nat
.
0.10
- Adapt to the
Semigroup
–Monoid
Proposal (introduced inbase-4.11
):- Add a
Semigroup
instance forDict
- Add the appropriate
(:=>)
instances involvingSemigroup
, and change theClass () (Monoid a)
instance toClass (Semigroup a) (Monoid a)
whenbase
is recent enough - Add the appropriate
Lifting(2)
instances involvingSemigroup
- Add a
Data.Constraint.Nat
now reexports theDiv
andMod
type families fromGHC.TypeLits
onbase-4.11
or later- Fix the type signature of
maxCommutes
- Export the
no
method ofBottom
- Add
NFData
instances forDict
and(:-)
0.9.1
- Correct an improper use of
unsafeCoerce
in the internals ofData.Constraint.Nat
andData.Constraint.Symbol
- Correctly identify the mismatched types when you defer an unsatisfiable
equality constraint through
Data.Constraint.Deferrable
- Re-export the
(:~~:)
defined inbase
fromData.Constraint.Deferred
with GHC 8.2 or later - Add several new
(:=>)
instances forBits
,Identity
,Const
,Natural
,IO
, andWord
. - Modernize some existing
Class
and(:=>)
instances to reflect the fact thatApplicative
is now a superclass ofMonad
on recent versions ofbase
.
0.9
- Changes to
Data.Constraint
:- Add
strengthen1
andstrengthen2
- Add
- Changes to
Data.Constraint.Deferrable
:- Add a
Deferrable ()
instance - The
Deferrable (a ~ b)
instance now shows theTypeRep
s ofa
andb
when a type mismatch error is thrown - Add
defer_
anddeferEither_
, counterparts todefer
anddeferEither
which do not require proxy arguments - Enable
PolyKinds
. This allows theDeferrable (a ~ b)
instance to be polykinded on all supported versions of GHC except 7.10, where the kinds must be*
due to an old GHC bug - Introduce a heterogeneous equality type
(:~~:)
, and use it to define aDeferrable (a ~~ b)
instance on GHC 8.0 or later
- Add a
- Changes to
Data.Constraint.Forall
:- Implement
ForallF
andForallT
in terms ofForall
- Add
ForallV
andInstV
(supporting a variable number of parameters) - Add a
forall
combinator
- Implement
- Introduce
Data.Constraint.Nat
andData.Constraint.Symbol
, which contain utilities for working withKnownNat
andKnownSymbol
constraints, respectively. These modules are only available on GHC 8.0 or later.
0.8
- GHC 8 compatibility
transformers
0.5 compatibilitybinary
0.8 compatibility- Dropped support for GHC 7.6 in favor of a nicer Bottom representation.
0.7
- Found a nicer encoding of the initial object in the category of constraints using a nullary constraint.
0.6.1
- Remove the need for closed type families from the new
Forall
.
0.6
- Completely redesigned
Data.Constraint.Forall
. The old design is unsound and can be abused to defineunsafeCoerce
! The new design requires closed type families, so this module now requires GHC 7.8+
0.5.1
- Added
Data.Constraint.Deferrable
.
0.5
- Added
Data.Constraint.Lifting
.
0.4.1.3
- Acknowledge we actually need at least base 4.5
0.4.1.2
- Restore support for building on older GHCs
0.4.1.1
- Minor documentation fixes.
0.4.1
- Added
mapDict
andunmapDict
. - Added a lot of documentation.
0.4
Typeable
andData
. TheData
instance for(:-)
is a conservative approximation that avoids having to turn (:-) into a cartesian closed category. If it becomes a pain point for users, I know how to do that, and have done so in other libraries – see hask, but I’m hesitant to bring such heavy machinery to bear and it isn’t clear how to do it in a way that is compatible with those other libraries.
0.3.5
- Explicit role annotations
0.3.4.1
- Fixed build failures.
- Fixed an unused import warning on older GHCs.
0.3.4
- Added
bottom