Safe Haskell | Safe-Infered |
---|
Existential datatypes holding evidence of constraints and type classes for existential datatypes.
- data Exists c where
- class Existential e where
- type ConstraintOf e :: * -> Constraint
- exists :: ConstraintOf e a => a -> e
- apply :: (forall a. ConstraintOf e a => a -> r) -> e -> r
- class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e
- translate :: (ExistentialWith c e1, ExistentialWith c e2) => e1 -> e2
- data Exists1 c a where
- class Existential1 e where
- type ConstraintOf1 e :: (* -> *) -> Constraint
- exists1 :: ConstraintOf1 e f => f a -> e a
- apply1 :: (forall f. ConstraintOf1 e f => f a -> r) -> e a -> r
- class (Existential1 e, c ~ ConstraintOf1 e) => ExistentialWith1 c e
- translate1 :: (ExistentialWith1 c e1, ExistentialWith1 c e2) => e1 a -> e2 a
- data Constraint
For kind *
A datatype which holds a value of a type satisfying the constraint c
, hiding the type, and evidence for the constraint, so that it can be retrieved by pattern matching later.
Example:
foo :: Exists Show foo = Exists (Just 9 :: Maybe Int) printExists :: Exists Show -> IO () printExists (Exists e) = print e main = printExists foo -- prints "Just 9"
Show (Exists Show) | |
Existential (Exists c) |
|
class Existential e whereSource
A type class to abstract over existential datatypes.
Example:
data EShow where EShow :: Show a => a -> EShow instance Existential EShow where type ConstraintOf EShow = Show exists = EShow apply f (EShow a) = f a foo :: EShow foo = exists (Just 9 :: Maybe Int) main = apply print foo -- prints "Just 9"
Note that had we given foo
the type signature
foo :: (Existential e, ConstraintOf e ~ Show) => e
GHC would have output an error message, because the instance of
to use would have been ambiguous. (The Existential
problem is the same as the apply
f .
exists
problem.)
show
.
read
type ConstraintOf e :: * -> ConstraintSource
exists :: ConstraintOf e a => a -> eSource
Construct e
from a value of a type satisfying the constraint.
apply :: (forall a. ConstraintOf e a => a -> r) -> e -> rSource
Apply a function requiring the constraint to the held value.
class (Existential e, c ~ ConstraintOf e) => ExistentialWith c e Source
An alias for convenience.
foo :: ExistentialWith Show e => e -> IO ()
is equivalent to
foo :: (Existential e, ConstraintOf e ~ Show) => e -> IO ()
(Existential e, ~ (* -> Constraint) c (ConstraintOf e)) => ExistentialWith c e |
translate :: (ExistentialWith c e1, ExistentialWith c e2) => e1 -> e2Source
Translate between different existential datatypes holding evidence for the same constraint.
For kind * -> *
A * -> *
kinded version of
which holds a value of a type constructor applied to a type, hiding the type constructor, and evidence for a constraint on the type constructor.
Exists
ComonadEnv e (Exists1 (ComonadEnv e)) | |
ComonadStore s (Exists1 (ComonadStore s)) | |
ComonadTraced m (Exists1 (ComonadTraced m)) | |
Functor (Exists1 Functor) | |
Functor (Exists1 Traversable) | |
Functor (Exists1 Comonad) | |
Functor (Exists1 Extend) | |
Functor (Exists1 (ComonadEnv e)) | |
Functor (Exists1 (ComonadStore s)) | |
Functor (Exists1 (ComonadTraced m)) | |
Foldable (Exists1 Foldable) | |
Foldable (Exists1 Traversable) | |
Traversable (Exists1 Traversable) | |
Comonad (Exists1 Comonad) | |
Comonad (Exists1 (ComonadEnv e)) | |
Comonad (Exists1 (ComonadStore s)) | |
Comonad (Exists1 (ComonadTraced m)) | |
Extend (Exists1 Comonad) | |
Extend (Exists1 Extend) | |
Extend (Exists1 (ComonadEnv e)) | |
Extend (Exists1 (ComonadStore s)) | |
Extend (Exists1 (ComonadTraced m)) | |
Contravariant (Exists1 Contravariant) | |
Copointed (Exists1 Copointed) | |
Existential1 (Exists1 c) |
|
class Existential1 e whereSource
A version of
for kind Existential
* -> *
.
type ConstraintOf1 e :: (* -> *) -> ConstraintSource
exists1 :: ConstraintOf1 e f => f a -> e aSource
Construct e
from a value of a type constructor applied to a type where the type constructor satisfies the constraint.
apply1 :: (forall f. ConstraintOf1 e f => f a -> r) -> e a -> rSource
Apply a function requiring the constraint to the held value.
Existential1 Anything1 |
|
Existential1 (Any (* -> *)) |
|
Existential1 (Exists1 c) |
|
class (Existential1 e, c ~ ConstraintOf1 e) => ExistentialWith1 c e Source
An alias for convenience. A version of ExistentialWith
for kind * -> *
.
(Existential1 e, ~ ((* -> *) -> Constraint) c (ConstraintOf1 e)) => ExistentialWith1 c e |
translate1 :: (ExistentialWith1 c e1, ExistentialWith1 c e2) => e1 a -> e2 aSource
Translate between different existential datatypes holding evidence for the same constraint on a * -> *
kinded type constructor.
The Constraint
kind
data Constraint