trivial-constraint 0.5.1.0 → 0.6.0.0

raw patch · 2 files changed

+152/−60 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• src/Data/Constraint/Trivial.hs +99/−53
• trivial-constraint.cabal +53/−7

@@ -7,52 +7,114 @@ {-# LANGUAGE ConstraintKinds         #-} {-# LANGUAGE DataKinds               #-} {-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE FlexibleContexts        #-} {-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE Rank2Types              #-}+{-# LANGUAGE EmptyCase               #-} {-# LANGUAGE PolyKinds               #-} {-# LANGUAGE TypeOperators           #-} {-# LANGUAGE UndecidableInstances    #-} {-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE AllowAmbiguousTypes     #-}  module Data.Constraint.Trivial (-            Unconstrained, Impossible(..)-          , Unconstrained2, Impossible2(..)-          , Unconstrained3, Impossible3(..)-          , Unconstrained4, Impossible4(..)-          , Unconstrained5, Impossible5(..)-          , Unconstrained6, Impossible6(..)-          , Unconstrained7, Impossible7(..)-          , Unconstrained8, Impossible8(..)-          , Unconstrained9, Impossible9(..)+          -- * Trivial classes+            Unconstrained0, Impossible0+          , Unconstrained, Impossible+          , Unconstrained2, Impossible2+          , Unconstrained3, Impossible3+          , Unconstrained4, Impossible4+          , Unconstrained5, Impossible5+          , Unconstrained6, Impossible6+          , Unconstrained7, Impossible7+          , Unconstrained8, Impossible8+          , Unconstrained9, Impossible9+          -- * Utility+          , Disallowed, nope           ) where  import           GHC.TypeLits+import           GHC.Exts (Any, TYPE) -type Disallowed t = 'Text "All instances of "-              ':<>: 'Text t-              ':<>: 'Text " are disallowed."+class Any => Bottom where+  no :: a+class (Bottom, TypeError ('Text "All instances of "+          ':<>: 'Text t+          ':<>: 'Text " are disallowed.")) => Disallowed t --- | Intended to be used as an argument for some type constructor which expects kind---   @k -> Constraint@, when you do not actually wish to constrain anything with it.+-- | A term-level witness that the context contains a 'Disallowed' constraint, i.e.+--   one of the 'Impossible0', 'Impossible' ... constraints. In such a context, because+--   you are guaranteed that it can under no circumstances actually be invoked, you+--   are allowed to to anything whatsoever, even create a value of an uninhabited unlifted+--   type.+nope :: forall (a :: TYPE rep). Bottom => a+nope = case no of++-- | A constraint that is always/unconditionally fulfilled. This behaves the same+--   way as @()@, when appearing in a constraint-tuple, i.e. it does not change anything+--   about the constraints. It is thus the identity of the @(,)@ monoid in the constraint+--   kind.+class Unconstrained0+instance Unconstrained0++-- | A constraint that never is fulfilled, in other words it is guaranteed that something+--   whose context contains this constraint will never actually be invoked in a program.+class Disallowed "Impossible0" => Impossible0+++-- | A parametric non-constraint. This can be used, for instance, when you have an+--   existential that contains endo-functions of any type of some specified constraint. -----   @'Unconstrained' t@ can always be added to the constraint list of any signature, without---   changing anything.+-- @+-- data GenEndo c where+--   GenEndo :: c a => (a -> a) -> GenEndo c+-- @+-- +--   Then, you can have values like @GenEndo abs :: GenEndo Num@. It is also possible+--   to have @GenEndo id :: GenEndo Num@, but here the num constraint is not actually+--   required. So what to use as the @c@ argument? It should be a constraint on a type+--   which does not actually constrain the type.+-- +-- @+-- idEndo :: GenEndo Unconstrained+-- idEndo = GenEndo id+-- @ class Unconstrained t instance Unconstrained t  --- | This constraint can /never/ be fulfilled. Might be useful e.g. as a default---   for a class-associated constraint; this basically disables any method with---   that constraint (so it can safely be left 'undefined').-class TypeError (Disallowed "Impossible") => Impossible t where-    -- | Ex falso quodlibet.  If you have @'Impossible' t@, you can do-    -- anything.-    ---    -- Might be useful e.g. if you are inside a function wiht an-    -- @'Impossible' t =>@ constraint, and you want to do something-    -- impossible, like the constraint implies.-    ---    -- Analogous to 'Data.Void.absurd'.-    absurdible :: proxy t -> a+-- | This constraint can /never/ be fulfilled. One application in which this can be+--   useful is as a default for a class-associated constraint; this basically disables+--   any method with that constraint: so it can safely be left 'undefined'. We provide+--   the 'nope' method as a special form of 'undefined', which actually guarantees it+--   is safe through the type system. For instance, the old monad class with+--   its controversial 'fail' method could be changed to+--+-- @+-- class Applicative m => Monad m where+--   (return,(>>=)) :: ...+--   type FailableResult m :: * -> Constraint+--   type FailableResult m = Impossible  -- fail disabled by default+--   fail :: FailableResult m a => String -> m a+--   fail = nope+-- @+-- +--   This would turn any use of fail in a “pure” monad (which does not actually+--   define 'fail') into a type error.+--   Meanwhile, “safe” uses of fail, such as in the IO monad, could be kept as-is,+--   by making the instance+--+-- @+-- instance Monad IO where+--   (return,(>>=)) = ...+--   type FailableResult m = Unconstrained+--   fail = throwErrow+-- @+-- +--   Other instances could support the 'fail' method only selectively for particular+--   result types, again by picking a suitable @FailableResult@ constraint+--   (e.g. 'Monoid').+class Disallowed "Impossible" => Impossible t   -- | Like 'Unconstrained', but with kind signature @k -> k -> Constraint@@@ -60,62 +122,46 @@ class Unconstrained2 t s instance Unconstrained2 t s -class TypeError (Disallowed "Impossible2") => Impossible2 t s where-    absurdible2 :: proxy t -> proxy s -> a+class Disallowed "Impossible2" => Impossible2 t s   class Unconstrained3 t s r instance Unconstrained3 t s r -class TypeError (Disallowed "Impossible3") => Impossible3 t s r where-    absurdible3 :: proxy t -> proxy s -> proxy r -> a+class Disallowed "Impossible3" => Impossible3 t s r   class Unconstrained4 t s r q instance Unconstrained4 t s r q -class TypeError (Disallowed "Impossible4") => Impossible4 t s r q where-    absurdible4 :: proxy t -> proxy s -> proxy r -> proxy q -> a+class Disallowed "Impossible4" => Impossible4 t s r q   class Unconstrained5 t s r q p instance Unconstrained5 t s r q p -class TypeError (Disallowed "Impossible5") => Impossible5 t s r q p where-    absurdible5 :: proxy t -> proxy s -> proxy r -> proxy q -> proxy p -> a+class Disallowed "Impossible5" => Impossible5 t s r q p   class Unconstrained6 t s r q p o instance Unconstrained6 t s r q p o -class TypeError (Disallowed "Impossible6") => Impossible6 t s r q p o where-    absurdible6 :: proxy t -> proxy s -> proxy r-                -> proxy q -> proxy p -> proxy o-                -> a+class Disallowed "Impossible6" => Impossible6 t s r q p o   class Unconstrained7 t s r q p o n instance Unconstrained7 t s r q p o n -class TypeError (Disallowed "Impossible7") => Impossible7 t s r q p o n where-    absurdible7 :: proxy t -> proxy s -> proxy r -> proxy q-                -> proxy p -> proxy o -> proxy n -> a+class Disallowed "Impossible7" => Impossible7 t s r q p o n   class Unconstrained8 t s r q p o n m instance Unconstrained8 t s r q p o n m -class TypeError (Disallowed "Impossible8") => Impossible8 t s r q p o n m where-    absurdible8 :: proxy t -> proxy s -> proxy r -> proxy q-                -> proxy p -> proxy o -> proxy n -> proxy m-                -> a+class Disallowed "Impossible8" => Impossible8 t s r q p o n m   class Unconstrained9 t s r q p o n m l instance Unconstrained9 t s r q p o n m l -class TypeError (Disallowed "Impossible9") => Impossible9 t s r q p o n m l where-    absurdible9 :: proxy t -> proxy s -> proxy r-                -> proxy q -> proxy p -> proxy o-                -> proxy n -> proxy m -> proxy l-                -> a+class Disallowed "Impossible9" => Impossible9 t s r q p o n m l

@@ -2,20 +2,66 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                trivial-constraint-version:             0.5.1.0+version:             0.6.0.0 synopsis:            Constraints that any type, resp. no type fulfills-description:         Since GHC 7.4, constraints are first-class: we have the constraint kind, and thus type-classes have a kind such as @* -> Constraint@.+description:         Since GHC 7.4, constraints are first-class: we have the constraint +                     kind, and thus type-classes have a kind of form @k -> Constraint@,+                     or @k -> l -> m -> ... -> Constraint@ for a multi-param type class.+                     Such type-level functions can be used as arguments to data types, or+                     as instances for other type classes.                      .-                     These can be used as parameters to data types. They also can be combined quite nicely,+                     For any given arity, the constraint-valued functions form a semigroup+                     with respect to “constraint intersection”, which Haskell supports with+                     tuple syntax, e.g.                      .                      @-                     type NewConstraint a = (Constraint1 a, Constraint2 a)+                     type NewCstrt¹ a = (Cstrt¹₀ a, Cstrt¹₁ a)                      @                      .-                     however you always need to start with a plain old type class when building constraints.+                     means that @NewCstrt¹ :: * -> Constraint@ requires that for+                     any given parameter both @Cstrt¹₀@ and @Cstrt¹₁@ be fulfilled.+                     It is intuitive enough that this type-level semigroup can be extended+                     to a monoid, but out of the box this is only possible for arity 0,+                     i.e. for @Cstrt⁰ :: Constraint@                      .-                     This library provides a type class that is not really a constraint at all, so you can "start from zero" with building up a custom constraint.-                     Also its opposite (a constraint that no type can ever fulfill).+                     @+                     (Cstrt⁰, ()) ~ ((), Cstrt⁰) ~ Cstrt⁰+                     @+                     .+                     For higher arity, this would require type-level lambdas, like for+                     @Cstrt² :: * -> * -> Constraint@+                     .+                     @+                     (Cstrt², \\a b -> ()) ~ (\\a b -> (), Cstrt²) ~ Cstrt²+                     @+                     .+                     which is not valid Haskell syntax. It is easy enough to define the+                     lambdas in an ad-hoc manner as+                     .+                     @+                     type Unconstrained² a b = ()+                     @+                     .+                     and then+                     .+                     @+                     (Cstrt², Unconstrained²) ~ (Unconstrained², Cstrt²) ~ Cstrt²+                     @+                     .+                     This library provides those /trivial constraints/ in+                     a single, documented place, and it uses classes instead of+                     type-synonyms (which would be problematic when it comes to partial+                     application). Arities 0-9 are provided.+                     .+                     They can be useful in any construction that is parameterised over a+                     constrainer-class, when you do /not/ wish to actually constrain the+                     domain with it.+                     .+                     The other thing this library provides are the opposite classes,+                     i.e. @\\a b ... -> Impossible@, constraints which can /never/ be +                     fulfilled. They are essentially dual to the @Unconstrained@ ones,+                     and can likewise be useful as parameters that should completely+                     “disable” a conditional feature. license:             GPL-3 license-file:        LICENSE author:              Justus Sagemüller