| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Constraint.Extras
Description
Throughout this module, we use the following GADT and ArgDict instance
in our examples:
{-# LANGUAGE StandaloneDeriving #-}
data Tag a where
I :: Tag Int
B :: Tag Bool
deriving instance Show (Tag a)
$(deriveArgDict ''Tag)The constructors of Tag mean that a type variable a in Tag a
must come from the set { Int, Bool }. We call this the "set of
types a that could be applied to Tag".
Synopsis
- class ArgDict (c :: k -> Constraint) (f :: k -> Type) where
- type ConstraintsFor f c :: Constraint
- argDict :: ConstraintsFor f c => f a -> Dict (c a)
- type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)
- argDict' :: forall f c g a. Has' c f g => f a -> Dict (c (g a))
- type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)
- argDictV :: forall f c g v. HasV c f g => f v -> Dict (c (v g))
- type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)
- has :: forall c f a r. Has c f => f a -> (c a => r) -> r
- type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)
- has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r
- type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)
- hasV :: forall c g f v r. HasV c f g => f v -> (c (v g) => r) -> r
- whichever :: forall c t a r. ForallF c t => (c (t a) => r) -> r
- class Implies1 c d where
- type ArgDictV f c = ArgDict f c
The ArgDict typeclass
class ArgDict (c :: k -> Constraint) (f :: k -> Type) where Source #
Morally, this class is for GADTs whose indices can be finitely
enumerated. An ArgDict c f
ConstraintsForrequests the set of constraintsc afor all possible typesathat could be applied tof.argDictselects a specificc agiven a value of typef a.
Use deriveArgDict to derive instances
of this class.
Associated Types
type ConstraintsFor f c :: Constraint Source #
Apply c to each possible type a that could appear in a f a.
ConstraintsFor Show Tag = (Show Int, Show Bool)
Methods
argDict :: ConstraintsFor f c => f a -> Dict (c a) Source #
Use an f a to select a specific dictionary from ConstraintsFor f c.
argDict I :: Dict (Show Int)
Instances
| (ArgDict c f, ArgDict c g) => ArgDict (c :: k -> Constraint) (Sum f g :: k -> Type) Source # | Since: 0.3.2.0 |
Defined in Data.Constraint.Extras Associated Types type ConstraintsFor (Sum f g) c Source # | |
| (ArgDict c f, ArgDict c g) => ArgDict (c :: k -> Constraint) (f :+: g :: k -> Type) Source # | Since: 0.3.2.0 |
Defined in Data.Constraint.Extras Associated Types type ConstraintsFor (f :+: g) c Source # | |
type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g) Source #
"Primed" variants (ConstraintsFor', argDict', Has',
has', &c.) use the ArgDict instance on f to apply constraints
on g a instead of just a. This is often useful when you have
data structures parameterised by something of kind (x -> Type) ->
Type, like in the dependent-sum and dependent-map libraries.
ConstraintsFor' Tag Show Identity = (Show (Identity Int), Show (Identity Bool))
argDict' :: forall f c g a. Has' c f g => f a -> Dict (c (g a)) Source #
Get a dictionary for a specific g a, using a value of type f a.
argDict' B :: Dict (Show (Identity Bool))
type ConstraintsForV (f :: (k -> k') -> Type) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g) Source #
Bringing instances into scope
type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c) Source #
Has c f is a constraint which means that for every type a
that could be applied to f, we have c a.
Has Show Tag = (ArgDict Show Tag, Show Int, Show Bool)
has :: forall c f a r. Has c f => f a -> (c a => r) -> r Source #
Use the a from f a to select a specific c a constraint, and
bring it into scope. The order of type variables is chosen to work
with -XTypeApplications.
-- Hold an a, along with a tag identifying the a. data SomeTagged tag where SomeTagged :: a -> tag a -> SomeTagged tag -- Use the stored tag to identify the thing we have, allowing us to call 'show'. Note that we -- have no knowledge of the tag type. showSomeTagged :: Has Show tag => SomeTagged tag -> String showSomeTagged (SomeTagged a tag) = has @Show tag $ show a
type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g) Source #
Has' c f g is a constraint which means that for every type a
that could be applied to f, we have c (g a).
Has' Show Tag Identity = (ArgDict (Show . Identity) Tag, Show (Identity Int), Show (Identity Bool))
has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r Source #
Like has, but we get a c (g a) instance brought into scope
instead. Use -XTypeApplications to specify c and g.
-- From dependent-sum:Data.Dependent.Sum data DSum tag f = forall a. !(tag a) :=> f a -- Show the value from a dependent sum. (We'll need 'whichever', discussed later, to show the key.) showDSumVal :: forall tag f . Has' Show tag f => DSum tag f -> String showDSumVal (tag :=> fa) = has' @Show @f tag $ show fa
whichever :: forall c t a r. ForallF c t => (c (t a) => r) -> r Source #
Given "forall a. c (t a)" (the ForallF c t constraint), select a
specific a, and bring c (t a) into scope. Use -XTypeApplications to
specify c, t and a.
-- Show the tag of a dependent sum, even though we don't know the tag type. showDSumKey :: forall tag f . ForallF Show tag => DSum tag f -> String showDSumKey ((tag :: tag a) :=> fa) = whichever @Show @tag @a $ show tag