constraints 0.8 → 0.9

raw patch · 9 files changed

+727/−84 lines, 9 filesdep −newtypedep −taggeddep ~basenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies removed: newtype, tagged

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +85/−0
• README.markdown +2/−0
• constraints.cabal +9/−8
• src/Data/Constraint.hs +31/−28
• src/Data/Constraint/Deferrable.hs +75/−9
• src/Data/Constraint/Forall.hs +82/−27
• src/Data/Constraint/Nat.hs +323/−0
• src/Data/Constraint/Symbol.hs +119/−0
• src/Data/Constraint/Unsafe.hs +1/−12

@@ -0,0 +1,85 @@+0.9+---+* Changes to `Data.Constraint`:+  * Add `strengthen1` and `strengthen2`+* Changes to `Data.Constraint.Deferrable`:+  * Add a `Deferrable ()` instance+  * The `Deferrable (a ~ b)` instance now shows the `TypeRep`s of `a` and `b`+    when a type mismatch error is thrown+  * Add `defer_` and `deferEither_`, counterparts to `defer` and `deferEither`+    which do not require proxy arguments+  * Enable `PolyKinds`. This allows the `Deferrable (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 a+    `Deferrable (a ~~ b)` instance on GHC 8.0 or later+* Changes to `Data.Constraint.Forall`:+  * Implement `ForallF` and `ForallT` in terms of `Forall`+  * Add `ForallV` and `InstV` (supporting a variable number of parameters)+  * Add a `forall` combinator+* Introduce `Data.Constraint.Nat` and `Data.Constraint.Symbol`, which contain+  utilities for working with `KnownNat` and `KnownSymbol` constraints,+  respectively. These modules are only available on GHC 8.0 or later.++0.8+-----+* GHC 8 compatibility+* `transformers` 0.5 compatibility+* `binary` 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](https://ghc.haskell.org/trac/ghc/ticket/7642).++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 define `unsafeCoerce`!+  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` and `unmapDict`.+* Added a lot of documentation.++0.4+---+* `Typeable` and `Data`. The `Data` 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](http://github.com/ekmett/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`

@@ -1,6 +1,8 @@ constraints =========== +[![Hackage](https://img.shields.io/hackage/v/constraints.svg)](https://hackage.haskell.org/package/constraints) [![Build Status](https://secure.travis-ci.org/ekmett/constraints.png?branch=master)](http://travis-ci.org/ekmett/constraints)+ This package provides data types and classes for manipulating the 'ConstraintKinds' exposed by GHC in 7.4.  Contact Information

@@ -1,7 +1,7 @@ name:          constraints category:      Constraints-version:       0.8-license:       BSD3+version:       0.9+license:       BSD2 cabal-version: >= 1.10 license-file:  LICENSE author:        Edward A. Kmett@@ -17,8 +17,9 @@   This package provides a vocabulary for working with them.  build-type:    Simple-tested-with:   GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.1, GHC == 7.10.2+tested-with:   GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.2 extra-source-files: README.markdown+                  , CHANGELOG.markdown  source-repository head   type: git@@ -50,16 +51,16 @@     transformers >= 0.2 && < 0.6,     transformers-compat >= 0.4 && < 1 -  if impl(ghc < 7.8)-    build-depends:-      newtype >= 0.2 && < 0.3,-      tagged >= 0.2 && < 1-   exposed-modules:     Data.Constraint     Data.Constraint.Deferrable     Data.Constraint.Forall     Data.Constraint.Lifting     Data.Constraint.Unsafe++  if impl(ghc >= 8)+    exposed-modules:+      Data.Constraint.Nat+      Data.Constraint.Symbol    ghc-options: -Wall

@@ -1,10 +1,13 @@ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RoleAnnotations #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-}@@ -13,11 +16,6 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 707-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE RoleAnnotations #-}-#endif #if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-} #endif@@ -58,10 +56,12 @@     Constraint   -- * Dictionary   , Dict(Dict)+  , withDict   -- * Entailment   , (:-)(Sub)   , (\\)   , weaken1, weaken2, contract+  , strengthen1, strengthen2   , (&&&), (***)   , trans, refl   , Bottom@@ -73,25 +73,17 @@   , Class(..)   , (:=>)(..)   ) where-import Control.Monad-#if __GLASGOW_HASKELL__ >= 707-import Control.Category-#endif import Control.Applicative+import Control.Category+import Control.Monad #if __GLASGOW_HASKELL__ < 710 import Data.Monoid #endif import Data.Complex import Data.Ratio-#if __GLASGOW_HASKELL__ >= 707 import Data.Data-#endif-#if __GLASGOW_HASKELL__ <= 710-import GHC.Prim (Constraint)-#else-import GHC.Types (Constraint)-#endif-import qualified GHC.Prim as Prim+import qualified GHC.Exts as Exts (Any)+import GHC.Exts (Constraint)  -- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@. --@@ -111,7 +103,6 @@ -- data Dict :: Constraint -> * where   Dict :: a => Dict a-#if __GLASGOW_HASKELL__ >= 707   deriving Typeable  @@ -128,12 +119,21 @@  dictDataType :: DataType dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]-#endif  deriving instance Eq (Dict a) deriving instance Ord (Dict a) deriving instance Show (Dict a) +-- | From a 'Dict', takes a value in an environment where the instance+-- witnessed by the 'Dict' is in scope, and evaluates it.+--+-- Essentially a deconstruction of a 'Dict' into its continuation-style+-- form.+--+withDict :: Dict a -> (a => r) -> r+withDict d r = case d of+                 Dict -> r+ infixr 9 :-  -- | This is the type of entailment.@@ -152,9 +152,10 @@ -- -- This relationship is captured in the ':-' entailment type here. ----- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a 'Category'--- of constraints. However, 'Category' only because sufficiently general to support this--- instance in GHC 7.8, so prior to 7.8 this instance is unavailable.+-- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a+-- 'Category' of constraints. However, 'Category' only became sufficiently+-- general to support this instance in GHC 7.8, so prior to 7.8 this instance+-- is unavailable. -- -- But due to the coherence of instance resolution in Haskell, this 'Category' -- has some very interesting properties. Notably, in the absence of@@ -190,7 +191,6 @@ -- library is sensible and can't break any assumptions on the behalf of -- library authors. newtype a :- b = Sub (a => Dict b)-#if __GLASGOW_HASKELL__ >= 707   deriving Typeable  type role (:-) nominal nominal@@ -218,7 +218,6 @@ instance Category (:-) where   id  = refl   (.) = trans-#endif  -- | Assumes 'IncoherentInstances' doesn't exist. instance Eq (a :- b) where@@ -279,6 +278,12 @@ weaken2 :: (a, b) :- b weaken2 = Sub Dict +strengthen1 :: Dict b -> a :- c -> a :- (b,c)+strengthen1 d e = unmapDict (const d) &&& e++strengthen2 :: Dict b -> a :- c -> a :- (c,b)+strengthen2 d e = e &&& unmapDict (const d)+ -- | Contracting a constraint / diagonal morphism -- -- The category of constraints is Cartesian. We can reuse information.@@ -305,8 +310,8 @@ top = Sub Dict  -- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance.-class Prim.Any => Bottom where-  no :: Dict a+class Exts.Any => Bottom where+  no :: a  -- | -- This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">@@ -331,9 +336,7 @@ unmapDict :: (Dict a -> Dict b) -> a :- b unmapDict f = Sub (f Dict) -#if __GLASGOW_HASKELL__ >= 707 type role Dict nominal-#endif  -------------------------------------------------------------------------------- -- Reflection

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ConstraintKinds #-}@@ -5,11 +6,18 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE PolyKinds #-} +#if __GLASGOW_HASKELL__ >= 800+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeInType #-}+#endif+ ----------------------------------------------------------------------------- -- | -- Module      :  Data.Constraint.Deferrable--- Copyright   :  (C) 2015 Edward Kmett+-- Copyright   :  (C) 2015-2016 Edward Kmett -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com>@@ -24,40 +32,98 @@   , Deferrable(..)   , defer   , deferred+#if __GLASGOW_HASKELL__ >= 800+  , defer_+  , deferEither_+  , (:~~:)(HRefl)+#endif+  , (:~:)(Refl)   ) where  import Control.Exception import Control.Monad import Data.Constraint import Data.Proxy-import Data.Typeable (Typeable, cast)+import Data.Typeable (Typeable, cast, typeRep)+import Data.Type.Equality ((:~:)(Refl)) +#if __GLASGOW_HASKELL__ >= 800+import GHC.Types (type (~~))+#endif+ data UnsatisfiedConstraint = UnsatisfiedConstraint String   deriving (Typeable, Show)  instance Exception UnsatisfiedConstraint  -- | Allow an attempt at resolution of a constraint at a later time-class Deferrable (p :: Constraint) where+class Deferrable p where   -- | Resolve a 'Deferrable' constraint with observable failure.   deferEither :: proxy p -> (p => r) -> Either String r  -- | Defer a constraint for later resolution in a context where we want to upgrade failure into an error-defer :: forall proxy p r. Deferrable p => proxy p -> (p => r) -> r-defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r +defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r+defer _ r = either (throw . UnsatisfiedConstraint) id $ deferEither (Proxy :: Proxy p) r  deferred :: forall p. Deferrable p :- p deferred = Sub $ defer (Proxy :: Proxy p) Dict --- We use our own type equality rather than @Data.Type.Equality@ to allow building on GHC 7.6.-data a :~: b where-  Refl :: a :~: a+#if __GLASGOW_HASKELL__ >= 800+-- | A version of 'defer' that uses visible type application in place of a 'Proxy'.+--+-- Only available on GHC 8.0 or later.+defer_ :: forall p r. Deferrable p => (p => r) -> r+defer_ r = defer @p Proxy r++-- | A version of 'deferEither' that uses visible type application in place of a 'Proxy'.+--+-- Only available on GHC 8.0 or later.+deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r+deferEither_ r = deferEither @p Proxy r+#endif++#if __GLASGOW_HASKELL__ >= 800+-- | Kind heterogeneous propositional equality. Like '(:~:)', @a :~~: b@ is+-- inhabited by a terminating value if and only if @a@ is the same type as @b@.+--+-- Only available on GHC 8.0 or later.+data (a :: i) :~~: (b :: j) where+  HRefl :: a :~~: a     deriving Typeable+#endif +showTypeRep :: Typeable t => Proxy t -> String+showTypeRep = show . typeRep++instance Deferrable () where+  deferEither _ r = Right r++-- | Deferrable homogeneous equality constraints.+--+-- Note that due to a GHC bug (https://ghc.haskell.org/trac/ghc/ticket/10343),+-- using this instance on GHC 7.10 will only work with @*@-kinded types.+#if __GLASGOW_HASKELL__ >= 800+instance (Typeable k, Typeable (a :: k), Typeable b) => Deferrable (a ~ b) where+#elif __GLASGOW_HASKELL__ == 710+instance (Typeable a, Typeable b) => Deferrable ((a :: *) ~ (b :: *)) where+#else instance (Typeable a, Typeable b) => Deferrable (a ~ b) where+#endif   deferEither _ r = case cast (Refl :: a :~: a) :: Maybe (a :~: b) of     Just Refl -> Right r-    Nothing -> Left "deferred type equality: type mismatch"+    Nothing   -> Left $+      "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `"  ++ showTypeRep (Proxy :: Proxy a) ++ "'"++#if __GLASGOW_HASKELL__ >= 800+-- | Deferrable heterogenous equality constraints.+--+-- Only available on GHC 8.0 or later.+instance (Typeable i, Typeable j, Typeable (a :: i), Typeable (b :: j)) => Deferrable (a ~~ b) where+  deferEither _ r = case cast (HRefl :: a :~~: a) :: Maybe (a :~~: b) of+    Just HRefl -> Right r+    Nothing   -> Left $+      "deferred type equality: type mismatch between `" ++ showTypeRep (Proxy :: Proxy a) ++ "’ and `"  ++ showTypeRep (Proxy :: Proxy a) ++ "'"+#endif  instance (Deferrable a, Deferrable b) => Deferrable (a, b) where   deferEither _ r = join $ deferEither (Proxy :: Proxy a) $ deferEither (Proxy :: Proxy b) r

@@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -7,6 +8,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE PolyKinds #-} #if __GLASGOW_HASKELL__ >= 800 {-# LANGUAGE UndecidableSuperClasses #-}@@ -15,7 +17,8 @@ -- | -- Module      :  Data.Constraint.Forall -- Copyright   :  (C) 2011-2015 Edward Kmett,---                (C) 2015 Ørjan Johansen+--                (C) 2015 Ørjan Johansen,+--                (C) 2016 David Feuer -- License     :  BSD-style (see the file LICENSE) -- -- Maintainer  :  Edward Kmett <ekmett@gmail.com>@@ -30,6 +33,8 @@   , ForallF, instF   , Forall1, inst1   , ForallT, instT+  , ForallV, InstV (instV)+  , forall   ) where  import Data.Constraint@@ -39,6 +44,14 @@  - for whether a class predicate holds, and if so assume that it holds for all  - types, unsafely coercing the typeclass dictionary.  -+ - The particular technique used to implement 'Forall' appears to have been+ - discovered first by Nicolas Frisby and is+ - <https://csks.wordpress.com/2012/10/22/safe-polykinded-universally-quantified-constraints-part-3-of-3/ discussed in some detail>+ - on his blog.+ -+ - However, his discovery did not directly affect the development of this+ - module.+ -  - A previous version of this module used concrete, unexported types as the  - skolems. This turned out to be unsound in the presence of type families.  - There were 3 somewhat distinct issues:@@ -85,17 +98,14 @@  - extract it from `Forall p` in order to tie the knot.  -} --- the `Skolem*` type families represent skolem variables, do not export!--- if GHC supports it, these might be made closed with no instances.+-- The `Skolem` type family represents skolem variables; do not export!+-- If GHC supports it, these might be made closed with no instances.  type family Skolem (p :: k -> Constraint) :: k-type family SkolemF (p :: k2 -> Constraint) (f :: k1 -> k2) :: k1-type family SkolemT1 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k1-type family SkolemT2 (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: k2 --- The outer `Forall*` type families prevent GHC from giving a spurious+-- The outer `Forall` type family prevents GHC from giving a spurious -- superclass cycle error.--- The inner `Forall*_` classes prevent the skolem from leaking to the user,+-- The inner `Forall_` class prevents the skolem from leaking to the user, -- which would be disastrous.  -- | A representation of the quantified constraint @forall a. p a@.@@ -104,33 +114,78 @@ class p (Skolem p) => Forall_ (p :: k -> Constraint) instance p (Skolem p) => Forall_ (p :: k -> Constraint) --- | A representation of the quantified constraint @forall a. p (f a)@.-type family ForallF (p :: k2 -> Constraint) (f :: k1 -> k2) :: Constraint-type instance ForallF p f = ForallF_ p f-class p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)-instance p (f (SkolemF p f)) => ForallF_ (p :: k2 -> Constraint) (f :: k1 -> k2)--type Forall1 p = Forall p---- | A representation of the quantified constraint @forall f a. p (t f a)@.-type family ForallT (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) :: Constraint-type instance ForallT p t = ForallT_ p t-class p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)-instance p (t (SkolemT1 p t) (SkolemT2 p t)) => ForallT_ (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3)- -- | Instantiate a quantified @'Forall' p@ constraint at type @a@. inst :: forall p a. Forall p :- p a inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p)) +-- | Composition for constraints.+class p (f a) => ComposeC (p :: k2 -> Constraint) (f :: k1 -> k2) (a :: k1)+instance p (f a) => ComposeC p f a++-- | A representation of the quantified constraint @forall a. p (f a)@.+class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint) (f :: k1 -> k2)+instance Forall (ComposeC p f) => ForallF p f+ -- | Instantiate a quantified @'ForallF' p f@ constraint at type @a@.-instF :: forall p f a. ForallF p f :- p (f a)-instF = unsafeCoerce (Sub Dict :: ForallF p f :- p (f (SkolemF p f)))+instF :: forall p f a . ForallF p f :- p (f a)+instF = Sub $+  case inst :: Forall (ComposeC p f) :- ComposeC p f a of+    Sub Dict -> Dict +-- Classes building up to ForallT+class p (t a b) => R (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1) (b :: k2)+instance p (t a b) => R p t a b+class Forall (R p t a) => Q (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (a :: k1)+instance Forall (R p t a) => Q p t a++-- | A representation of the quantified constraint @forall f a. p (t f a)@.+class Forall (Q p t) => ForallT (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4)+instance Forall (Q p t) => ForallT p t++-- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.+instT :: forall (p :: k4 -> Constraint) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)+instT = Sub $+  case inst :: Forall (Q p t) :- Q p t f of { Sub Dict ->+  case inst :: Forall (R p t f) :- R p t f a of+    Sub Dict -> Dict }++type Forall1 p = Forall p -- | Instantiate a quantified constraint on kind @* -> *@. -- This is now redundant since @'inst'@ became polykinded. inst1 :: forall (p :: (* -> *) -> Constraint) (f :: * -> *). Forall p :- p f inst1 = inst --- | Instantiate a quantified @'ForallT' p t@ constraint at types @f@ and @a@.-instT :: forall (p :: k3 -> Constraint) (t :: k1 -> k2 -> k3) (f :: k1) (a :: k2). ForallT p t :- p (t f a)-instT = unsafeCoerce (Sub Dict :: ForallT p t :- p (t (SkolemT1 p t) (SkolemT2 p t)))+-- | A representation of the quantified constraint+-- @forall a1 a2 ... an . p a1 a2 ... an@, supporting a variable number of+-- parameters.+type family ForallV :: k -> Constraint+type instance ForallV = ForallV_++class ForallV' p => ForallV_ (p :: k)+instance ForallV' p => ForallV_ p++-- | Instantiate a quantified @'ForallV' p@ constraint as @c@, where+-- @c ~ p a1 a2 ... an@.+class InstV (p :: k) c | k c -> p where+    type ForallV' (p :: k) :: Constraint+    instV :: ForallV p :- c++instance p ~ c => InstV (p :: Constraint) c where+    type ForallV' (p :: Constraint) = p+    instV = Sub Dict++-- Treating 1 argument specially rather than recursing as a bit of (premature?)+-- optimization+instance p a ~ c => InstV (p :: k -> Constraint) c where+    type ForallV' (p :: k -> Constraint) = Forall p+    instV = Sub $ case inst :: Forall p :- c of+        Sub Dict -> Dict++instance InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c where+    type ForallV' (p :: k1 -> k2 -> k3) = ForallF ForallV p+    instV = Sub $ case instF :: ForallF ForallV p :- ForallV (p a) of+        Sub Dict -> case instV :: ForallV (p a) :- c of+            Sub Dict -> Dict++forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)+forall d = case d :: Dict (p (Skolem p)) of Dict -> Dict

@@ -0,0 +1,323 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE Trustworthy #-}+-- | Utilities for working with 'KnownNat' constraints.+--+-- This module is only available on GHC 8.0 or later.+module Data.Constraint.Nat+  ( Min, Max, Lcm, Gcd, Divides, Div, Mod+  , plusNat, timesNat, powNat, minNat, maxNat, gcdNat, lcmNat, divNat, modNat+  , plusZero, timesZero, timesOne, powZero, powOne, maxZero, minZero, gcdZero, gcdOne, lcmZero, lcmOne+  , plusAssociates, timesAssociates, minAssociates, maxAssociates, gcdAssociates, lcmAssociates+  , plusCommutes, timesCommutes, minCommutes, maxCommutes, gcdCommutes, lcmCommutes+  , plusDistributesOverTimes, timesDistributesOverPow, timesDistributesOverGcd, timesDistributesOverLcm+  , minDistributesOverPlus, minDistributesOverTimes, minDistributesOverPow1, minDistributesOverPow2, minDistributesOverMax+  , maxDistributesOverPlus, maxDistributesOverTimes, maxDistributesOverPow1, maxDistributesOverPow2, maxDistributesOverMin+  , gcdDistributesOverLcm, lcmDistributesOverGcd+  , minIsIdempotent, maxIsIdempotent, lcmIsIdempotent, gcdIsIdempotent+  , plusIsCancellative, timesIsCancellative+  , dividesPlus, dividesTimes, dividesMin, dividesMax, dividesPow, dividesGcd, dividesLcm+  , plusMonotone1, plusMonotone2+  , timesMonotone1, timesMonotone2+  , powMonotone1, powMonotone2+  , minMonotone1, minMonotone2+  , maxMonotone1, maxMonotone2+  , divMonotone1, divMonotone2+  , euclideanNat+  , plusMod, timesMod+  , modBound+  , dividesDef+  , timesDiv+  , eqLe, leEq, leId, leTrans+  , leZero, zeroLe+  ) where++import Data.Constraint+import Data.Proxy+import GHC.TypeLits+import Unsafe.Coerce++type family Min :: Nat -> Nat -> Nat where+type family Max :: Nat -> Nat -> Nat where+type family Div :: Nat -> Nat -> Nat where+type family Mod :: Nat -> Nat -> Nat where+type family Gcd :: Nat -> Nat -> Nat where+type family Lcm :: Nat -> Nat -> Nat where++type Divides n m = n ~ Gcd n m++newtype Magic n r = Magic (KnownNat n => r)++magic :: forall n m o. (Integer -> Integer -> Integer) -> (KnownNat n, KnownNat m) :- KnownNat o+magic f = Sub $ unsafeCoerce (Magic id) (natVal (Proxy :: Proxy n) `f` natVal (Proxy :: Proxy m))++axiom :: forall a b. Dict (a ~ b)+axiom = unsafeCoerce (Dict :: Dict (a ~ a))++axiomLe :: forall a b. Dict (a <= b)+axiomLe = axiom++eqLe :: (a ~ b) :- (a <= b)+eqLe = Sub Dict++dividesGcd :: forall a b c. (Divides a b, Divides a c) :- Divides a (Gcd b c)+dividesGcd = Sub axiom++dividesLcm :: forall a b c. (Divides a c, Divides b c) :- Divides (Lcm a b) c+dividesLcm = Sub axiom++gcdCommutes :: forall a b. Dict (Gcd a b ~ Gcd b a)+gcdCommutes = axiom++lcmCommutes :: forall a b. Dict (Lcm a b ~ Lcm b a)+lcmCommutes = axiom++gcdZero :: forall a. Dict (Gcd 0 a ~ a)+gcdZero = axiom++gcdOne :: forall a. Dict (Gcd 1 a ~ 1)+gcdOne = axiom++lcmZero :: forall a. Dict (Lcm 0 a ~ 0)+lcmZero = axiom++lcmOne :: forall a. Dict (Lcm 1 a ~ a)+lcmOne = axiom++gcdNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Gcd n m)+gcdNat = magic gcd++lcmNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Lcm n m)+lcmNat = magic lcm++plusNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m)+plusNat = magic (+)++minNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Min n m)+minNat = magic min++maxNat   :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (Max n m)+maxNat = magic max++timesNat  :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m)+timesNat = magic (*)++powNat :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m)+powNat = magic (^)++divNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Div n m)+divNat = Sub $ case magic @n @m div of Sub r -> r++modNat :: forall n m. (KnownNat n, KnownNat m, 1 <= m) :- KnownNat (Mod n m)+modNat = Sub $ case magic @n @m mod of Sub r -> r++plusZero :: forall n. Dict ((n + 0) ~ n)+plusZero = axiom++timesZero :: forall n. Dict ((n * 0) ~ 0)+timesZero = axiom++timesOne :: forall n. Dict ((n * 1) ~ n)+timesOne = axiom++minZero :: forall n. Dict (Min n 0 ~ 0)+minZero = axiom++maxZero :: forall n. Dict (Max n 0 ~ n)+maxZero = axiom++powZero :: forall n. Dict ((n ^ 0) ~ 1)+powZero = axiom++leZero :: forall a. (a <= 0) :- (a ~ 0)+leZero = Sub axiom++zeroLe :: forall a. Dict (0 <= a)+zeroLe = axiom++plusMonotone1 :: forall a b c. (a <= b) :- (a + c <= b + c)+plusMonotone1 = Sub axiom++plusMonotone2 :: forall a b c. (b <= c) :- (a + b <= a + c)+plusMonotone2 = Sub axiom++powMonotone1 :: forall a b c. (a <= b) :- ((a^c) <= (b^c))+powMonotone1 = Sub axiom++powMonotone2 :: forall a b c. (b <= c) :- ((a^b) <= (a^c))+powMonotone2 = Sub axiom++divMonotone1 :: forall a b c. (a <= b) :- (Div a c <= Div b c)+divMonotone1 = Sub axiom++divMonotone2 :: forall a b c. (b <= c) :- (Div a c <= Div a b)+divMonotone2 = Sub axiom++timesMonotone1 :: forall a b c. (a <= b) :- (a * c <= b * c)+timesMonotone1 = Sub axiom++timesMonotone2 :: forall a b c. (b <= c) :- (a * b <= a * c)+timesMonotone2 = Sub axiom++minMonotone1 :: forall a b c. (a <= b) :- (Min a c <= Min b c)+minMonotone1 = Sub axiom++minMonotone2 :: forall a b c. (b <= c) :- (Min a b <= Min a c)+minMonotone2 = Sub axiom++maxMonotone1 :: forall a b c. (a <= b) :- (Max a c <= Max b c)+maxMonotone1 = Sub axiom++maxMonotone2 :: forall a b c. (b <= c) :- (Max a b <= Max a c)+maxMonotone2 = Sub axiom++powOne :: forall n. Dict ((n ^ 1) ~ n)+powOne = axiom++plusMod :: forall a b c. (1 <= c) :- (Mod (a + b) c ~ Mod (Mod a c + Mod b c) c)+plusMod = Sub axiom++timesMod :: forall a b c. (1 <= c) :- (Mod (a * b) c ~ Mod (Mod a c * Mod b c) c)+timesMod = Sub axiom++modBound :: forall m n. (1 <= n) :- (Mod m n <= n)+modBound = Sub axiom++euclideanNat :: (1 <= c) :- (a ~ (c * Div a c + Mod a c))+euclideanNat = Sub axiom++plusCommutes :: forall n m. Dict ((m + n) ~ (n + m))+plusCommutes = axiom++timesCommutes :: forall n m. Dict ((m * n) ~ (n * m))+timesCommutes = axiom++minCommutes :: forall n m. Dict (Min m n ~ Min n m)+minCommutes = axiom++maxCommutes :: forall n m. Dict (Min m n ~ Min n m)+maxCommutes = axiom++plusAssociates :: forall n m o. Dict (((m + n) + o) ~ (m + (n + o)))+plusAssociates = axiom++timesAssociates :: forall n m o. Dict (((m * n) * o) ~ (m * (n * o)))+timesAssociates = axiom++minAssociates :: forall n m o. Dict (Min (Min m n) o ~ Min m (Min n o))+minAssociates = axiom++maxAssociates :: forall n m o. Dict (Max (Max m n) o ~ Max m (Max n o))+maxAssociates = axiom++gcdAssociates :: forall a b c. Dict (Gcd (Gcd a b) c  ~ Gcd a (Gcd b c))+gcdAssociates = axiom++lcmAssociates :: forall a b c. Dict (Lcm (Lcm a b) c ~ Lcm a (Lcm b c))+lcmAssociates = axiom++minIsIdempotent :: forall n. Dict (Min n n ~ n)+minIsIdempotent = axiom++maxIsIdempotent :: forall n. Dict (Max n n ~ n)+maxIsIdempotent = axiom++gcdIsIdempotent :: forall n. Dict (Gcd n n ~ n)+gcdIsIdempotent = axiom++lcmIsIdempotent :: forall n. Dict (Lcm n n ~ n)+lcmIsIdempotent = axiom++minDistributesOverPlus :: forall n m o. Dict ((n + Min m o) ~ Min (n + m) (n + o))+minDistributesOverPlus = axiom++minDistributesOverTimes :: forall n m o. Dict ((n * Min m o) ~ Min (n * m) (n * o))+minDistributesOverTimes = axiom++minDistributesOverPow1 :: forall n m o. Dict ((Min n m ^ o) ~ Min (n ^ o) (m ^ o))+minDistributesOverPow1 = axiom++minDistributesOverPow2 :: forall n m o. Dict ((n ^ Min m o) ~ Min (n ^ m) (n ^ o))+minDistributesOverPow2 = axiom++minDistributesOverMax :: forall n m o. Dict (Max n (Min m o) ~ Min (Max n m) (Max n o))+minDistributesOverMax = axiom++maxDistributesOverPlus :: forall n m o. Dict ((n + Max m o) ~ Max (n + m) (n + o))+maxDistributesOverPlus = axiom++maxDistributesOverTimes :: forall n m o. Dict ((n * Max m o) ~ Max (n * m) (n * o))+maxDistributesOverTimes = axiom++maxDistributesOverPow1 :: forall n m o. Dict ((Max n m ^ o) ~ Max (n ^ o) (m ^ o))+maxDistributesOverPow1 = axiom++maxDistributesOverPow2 :: forall n m o. Dict ((n ^ Max m o) ~ Max (n ^ m) (n ^ o))+maxDistributesOverPow2 = axiom++maxDistributesOverMin :: forall n m o. Dict (Min n (Max m o) ~ Max (Min n m) (Min n o))+maxDistributesOverMin = axiom++plusDistributesOverTimes :: forall n m o. Dict ((n * (m + o)) ~ (n * m + n * o))+plusDistributesOverTimes = axiom++timesDistributesOverPow  :: forall n m o. Dict ((n ^ (m + o)) ~ (n ^ m * n ^ o))+timesDistributesOverPow = axiom++timesDistributesOverGcd :: forall n m o. Dict ((n * Gcd m o) ~ Gcd (n * m) (n * o))+timesDistributesOverGcd = axiom++timesDistributesOverLcm :: forall n m o. Dict ((n * Lcm m o) ~ Lcm (n * m) (n * o))+timesDistributesOverLcm = axiom++plusIsCancellative :: forall n m o. ((n + m) ~ (n + o)) :- (m ~ o)+plusIsCancellative = Sub axiom++timesIsCancellative :: forall n m o. (1 <= n, (n * m) ~ (n * o)) :- (m ~ o)+timesIsCancellative = Sub axiom++gcdDistributesOverLcm :: forall a b c. Dict (Gcd (Lcm a b) c ~ Lcm (Gcd a c) (Gcd b c))+gcdDistributesOverLcm = axiom++lcmDistributesOverGcd :: forall a b c. Dict (Lcm (Gcd a b) c ~ Gcd (Lcm a c) (Lcm b c))+lcmDistributesOverGcd = axiom++dividesPlus :: (Divides a b, Divides a c) :- Divides a (b + c)+dividesPlus = Sub axiom++dividesTimes :: (Divides a b, Divides a c) :- Divides a (b * c)+dividesTimes = Sub axiom++dividesMin :: (Divides a b, Divides a c) :- Divides a (Min b c)+dividesMin = Sub axiom++dividesMax :: (Divides a b, Divides a c) :- Divides a (Max b c)+dividesMax = Sub axiom++dividesDef :: forall a b. Divides a b :- ((a * Div b a) ~ a)+dividesDef = Sub axiom++dividesPow :: (1 <= n, Divides a b) :- Divides a (b^n)+dividesPow = Sub axiom++timesDiv :: forall a b. Dict ((a * Div b a) <= a)+timesDiv = axiom++-- (<=) is an internal category in the category of constraints.++leId :: forall a. Dict (a <= a)+leId = Dict++leEq :: forall a b. (a <= b, b <= a) :- (a ~ b)+leEq = Sub axiom++leTrans :: forall a b c. (b <= c, a <= b) :- (a <= c)+leTrans = Sub (axiomLe @a @c)

@@ -0,0 +1,119 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+-- | Utilities for working with 'KnownSymbol' constraints.+--+-- This module is only available on GHC 8.0 or later.+module Data.Constraint.Symbol+  ( type (++)+  , type Take+  , type Drop+  , type Length+  , appendSymbol+  , appendUnit1+  , appendUnit2+  , appendAssociates+  , takeSymbol+  , dropSymbol+  , takeAppendDrop+  , lengthSymbol+  , takeLength+  , take0+  , takeEmpty+  , dropLength+  , drop0+  , dropEmpty+  , lengthTake+  , lengthDrop+  , dropDrop+  , takeTake+  ) where++import Data.Constraint+import Data.Constraint.Nat+import Data.Proxy+import GHC.TypeLits+import Unsafe.Coerce++type family (++) :: Symbol -> Symbol -> Symbol where+type family Take :: Nat -> Symbol -> Symbol where+type family Drop :: Nat -> Symbol -> Symbol where+type family Length :: Symbol -> Nat where++-- implementation details++newtype Magic n r = Magic (KnownSymbol n => r)++magicNSS :: forall n m o. (Int -> String -> String) -> (KnownNat n, KnownSymbol m) :- KnownSymbol o+magicNSS f = Sub $ unsafeCoerce (Magic id) (fromIntegral (natVal (Proxy :: Proxy n)) `f` symbolVal (Proxy :: Proxy m))++magicSSS :: forall n m o. (String -> String -> String) -> (KnownSymbol n, KnownSymbol m) :- KnownSymbol o+magicSSS f = Sub $ unsafeCoerce (Magic id) (symbolVal (Proxy :: Proxy n) `f` symbolVal (Proxy :: Proxy m))++magicSN :: forall a n. (String -> Int) -> KnownSymbol a :- KnownNat n+magicSN f = Sub $ unsafeCoerce (Magic id) (toInteger (f (symbolVal (Proxy :: Proxy a))))++axiom :: forall a b. Dict (a ~ b)+axiom = unsafeCoerce (Dict :: Dict (a ~ a))++-- axioms and operations++appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b)+appendSymbol = magicSSS (++)++appendUnit1 :: forall a. Dict (("" ++ a) ~ a)+appendUnit1 = axiom++appendUnit2 :: forall a. Dict ((a ++ "") ~ a)+appendUnit2 = axiom++appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))+appendAssociates = axiom++takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)+takeSymbol = magicNSS take++dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)+dropSymbol = magicNSS drop++takeAppendDrop :: forall n a. Dict (Take n a ++ Drop n a ~ a)+takeAppendDrop = axiom++lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a)+lengthSymbol = magicSN length++takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a)+takeLength = Sub axiom++take0 :: forall a. Dict (Take 0 a ~ "")+take0 = axiom++takeEmpty :: forall n. Dict (Take n "" ~ "")+takeEmpty = axiom++dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "")+dropLength = Sub axiom++drop0 :: forall a. Dict (Drop 0 a ~ a)+drop0 = axiom++dropEmpty :: forall n. Dict (Drop n "" ~ "")+dropEmpty = axiom++lengthTake :: forall n a. Dict (Length (Take n a) <= n)+lengthTake = axiom++lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n))+lengthDrop = axiom++dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a)+dropDrop = axiom++takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a)+takeTake = axiom

@@ -32,20 +32,9 @@  import Control.Applicative import Control.Monad+import Data.Coerce import Data.Constraint import Unsafe.Coerce--#if __GLASGOW_HASKELL__ >= 708--import Data.Coerce--#else--import Control.Newtype--type Coercible = Newtype--#endif  -- | Coerce a dictionary unsafely from one type to another unsafeCoerceConstraint :: a :- b