darcs-2.8.5: a distributed, interactive, smart revision control system

Safe HaskellNone
LanguageHaskell98

Darcs.Witnesses.Sealed

Synopsis

Documentation

data Sealed a where Source

Constructors

Sealed :: a x -> Sealed a 

Instances

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

seal :: a x -> Sealed a Source

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

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

data Sealed2 a where Source

Constructors

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

Instances

Show2 a => Show (Sealed2 a) 

seal2 :: a x y -> Sealed2 a Source

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

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

data FlippedSeal a y where Source

Constructors

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

flipSeal :: a x y -> FlippedSeal a y Source

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

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

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

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

class Gap w where Source

Gap abstracts over FreeLeft and FreeRight for code constructing these values

Methods

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

An empty Gap, e.g. NilFL or NilRL

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

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 Source

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

data FreeLeft p Source

'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

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

Unwrap a FreeLeft value

data FreeRight p Source

'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