| 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 Has c f where
- argDict' :: forall c g f a. Has' c f g => f a -> Dict (c (g a))
- argDictV :: forall f c g v. HasV c f g => f v -> Dict (c (v g))
- type Has' (c :: k -> Constraint) f (g :: k' -> k) = Has (ComposeC c g) f
- has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r
- type HasV c f g = Has (FlipC (ComposeC c) g) f
- 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
The Has typeclass
The constraint Has c f means that given any value of type f a, we can determine
that there is an instance of c a. For example, Has Show Tag means that given any
x :: Tag a, we can conclude Show a. Most commonly, the type f will be a GADT,
where we can enumerate all the possible index types through pattern matching, and
discover that there is an appropriate instance in each case. In this sort of
situation, the c can be left entirely polymorphic in the instance for Has, and
this is the sort of instance that the provided Template Haskell code writes.
Methods
has :: forall a r. f a -> (c a => r) -> r Source #
Use the f a to show that there is an instance of c a, and
bring it into scope.
The order of type variables is chosen to work
with -XTypeApplications.
-- Hold a value of type 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
argDict :: forall a. f a -> Dict (c a) Source #
Use an f a to obtain a dictionary for c a
argDict @Show I :: Dict (Show Int)
argDict' :: forall c g f a. Has' c f g => f a -> Dict (c (g a)) Source #
Get a dictionary for c (g a), using a value of type f a.
argDict' @Show @Identity B :: Dict (Show (Identity Bool))
argDictV :: forall f c g v. HasV c f g => f v -> Dict (c (v g)) Source #
Get a dictionary for c (v g), using a value of type f v.
Bringing instances into scope
type Has' (c :: k -> Constraint) f (g :: k' -> k) = Has (ComposeC c g) f Source #
The constraint Has' c f g means that given a value of type f a, we can satisfy the constraint c (g a).
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
type HasV c f g = Has (FlipC (ComposeC c) g) f Source #
The constraint HasV c f g means that given a value of type f v, we can satisfy the constraint c (v g).
hasV :: forall c g f v r. HasV c f g => f v -> (c (v g) => r) -> r Source #
Similar to has, but given a value of type f v, we get a c (v g) instance brought into scope instead.
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