| 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