Darcs.Witnesses.Sealed

Documentation

data Sealed a where

Constructors

Sealed :: a x -> Sealed a

Instances

MyEq a => Eq (Sealed (a x))

Show1 a => Show (Sealed a)

seal :: a x -> Sealed a

unseal :: (forall x. a x -> b) -> Sealed a -> b

mapSeal :: (forall x. a x -> b x) -> Sealed a -> Sealed b

unsafeUnseal :: Sealed a -> a x

unsafeUnsealFlipped :: FlippedSeal a y -> a x y

unsafeUnseal2 :: Sealed2 a -> a x y

data Sealed2 a where

Constructors

Sealed2 :: !(a x y) -> Sealed2 a

Instances

Show2 a => Show (Sealed2 a)

seal2 :: a x y -> Sealed2 a

unseal2 :: (forall x y. a x y -> b) -> Sealed2 a -> b

mapSeal2 :: (forall x y. a x y -> b x y) -> Sealed2 a -> Sealed2 b

data FlippedSeal a y where

Constructors

FlippedSeal :: !(a x y) -> FlippedSeal a y

flipSeal :: a x y -> FlippedSeal a y

unsealFlipped :: (forall x y. a x y -> b) -> FlippedSeal a z -> b

mapFlipped :: (forall x. a x y -> b x z) -> FlippedSeal a y -> FlippedSeal b z

unsealM :: Monad m => m (Sealed a) -> (forall x. a x -> m b) -> m b

liftSM :: Monad m => (forall x. a x -> b) -> m (Sealed a) -> m b

class Gap w where

Gap abstracts over FreeLeft and FreeRight for code constructing these values

Methods

emptyGap :: (forall x. p x x) -> w p

An empty Gap, e.g. NilFL or NilRL

freeGap :: (forall x y. p x y) -> w p

A Gap constructed from a completely polymorphic value, for example the constructors for primitive patches

joinGap :: (forall x y z. p x y -> q y z -> r x z) -> w p -> w q -> w r

Compose two Gap values together in series, e.g. 'joinGap (+>+)' or 'joinGap (:>:)'

Instances

Gap FreeRight

Gap FreeLeft

data FreeLeft p

'FreeLeft p' is 'forall x . exists y . p x y' In other words the caller is free to specify the left witness, and then the right witness is an existential. Note that the order of the type constructors is important for ensuring that y is dependent on the x that is supplied. This is why Stepped is needed, rather than writing the more obvious 'Sealed (Poly p)' which would notionally have the same quantification of the type witnesses.

Instances

Gap FreeLeft

unFreeLeft :: FreeLeft p -> Sealed (p x)

Unwrap a FreeLeft value

data FreeRight p

'FreeLeft p' is 'forall y . exists x . p x y' In other words the caller is free to specify the right witness, and then the left witness is an existential. Note that the order of the type constructors is important for ensuring that x is dependent on the y that is supplied.

Instances

Gap FreeRight

unFreeRight :: FreeRight p -> FlippedSeal p x

Unwrap a FreeRight value