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

Safe HaskellSafe-Infered

Darcs.Witnesses.Sealed

Synopsis

Documentation

data Sealed a whereSource

Constructors

Sealed :: a x -> Sealed a 

Instances

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

seal :: a x -> Sealed aSource

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

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

data Sealed2 a whereSource

Constructors

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

Instances

Show2 a => Show (Sealed2 a) 

seal2 :: a x y -> Sealed2 aSource

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

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

data FlippedSeal a y whereSource

Constructors

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

flipSeal :: a x y -> FlippedSeal a ySource

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

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

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

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

class Gap w whereSource

Gap abstracts over FreeLeft and FreeRight for code constructing these values

Methods

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

An empty Gap, e.g. NilFL or NilRL

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

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 rSource

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