exists-0.1: Existential datatypes holding evidence of constraints

Safe HaskellSafe-Infered

Data.Exists

Contents

Description

Existential datatypes holding evidence of constraints and type classes for existential datatypes.

Synopsis

For kind *

data Exists c whereSource

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"

Constructors

Exists :: c a => a -> Exists c 

Instances

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 Existential to use would have been ambiguous. (The apply f . exists problem is the same as the show . read problem.)

Associated Types

type ConstraintOf e :: * -> ConstraintSource

Methods

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.

Instances

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 ()

Instances

(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 * -> *

data Exists1 c a whereSource

A * -> * kinded version of Exists 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.

Constructors

Exists1 :: c f => f a -> Exists1 c a 

Instances

class Existential1 e whereSource

A version of Existential for kind * -> *.

Associated Types

type ConstraintOf1 e :: (* -> *) -> ConstraintSource

Methods

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.

Instances

class (Existential1 e, c ~ ConstraintOf1 e) => ExistentialWith1 c e Source

An alias for convenience. A version of ExistentialWith for kind * -> *.

Instances

(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