diff --git a/src/Data/Constraint/Trivial.hs b/src/Data/Constraint/Trivial.hs --- a/src/Data/Constraint/Trivial.hs +++ b/src/Data/Constraint/Trivial.hs @@ -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 diff --git a/trivial-constraint.cabal b/trivial-constraint.cabal --- a/trivial-constraint.cabal +++ b/trivial-constraint.cabal @@ -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