Safe Haskell	None
Language	Haskell2010

Darcs.Patch.Witnesses.Sealed

Synopsis

Documentation

data Sealed a where Source

A Sealed type is a way of hide an existentially quantified type parameter, in this case wX, inside the type. Note that the only thing we can currently recover about the existentially quantified type wX is that it exists.

Constructors

Sealed :: a wX -> Sealed a

Instances

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

seal :: a wX -> Sealed a Source

data Sealed2 a where Source

The same as Sealed but for two parameters (wX and wY).

Constructors

Sealed2 :: !(a wX wY) -> Sealed2 a

Instances

Show2 a => Show (Sealed2 a)

seal2 :: a wX wY -> Sealed2 a Source

data FlippedSeal a wY where Source

Constructors

FlippedSeal :: !(a wX wY) -> FlippedSeal a wY

flipSeal :: a wX wY -> FlippedSeal a wY Source

unsafeUnseal :: Sealed a -> a wX Source

unsafeUnsealFlipped :: FlippedSeal a wY -> a wX wY Source

unsafeUnseal2 :: Sealed2 a -> a wX wY Source

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

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

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

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

mapFlipped :: (forall wX. a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ Source

unseal2 :: (forall wX wY. a wX wY -> b) -> Sealed2 a -> b Source

mapSeal2 :: (forall wX wY. a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b Source

unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b Source

newtype Poly a Source

Poly is similar to Sealed, but the type argument is universally quantified instead of being existentially quantified.

Constructors

Poly
Fields unPoly :: forall wX. a wX

newtype Stepped f a wX Source

Stepped is a type level composition operator. For example, Stepped (Sealed p) is equivalent to \x -> Sealed (p x)

Constructors

Stepped
Fields unStepped :: f (a wX)

newtype 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.

Constructors

FLInternal (Poly (Stepped Sealed p))

Instances

Gap FreeLeft

newtype 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.

Constructors

FRInternal (Poly (FlippedSeal p))

Instances

Gap FreeRight

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

Unwrap a FreeLeft value

unFreeRight :: FreeRight p -> FlippedSeal p wX Source

Unwrap a FreeRight value

class Gap w where Source

Gap abstracts over FreeLeft and FreeRight for code constructing these values

Methods

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

An empty Gap, e.g. NilFL or NilRL

freeGap :: (forall wX wY. p wX wY) -> w p Source

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

joinGap :: (forall wX wY wZ. p wX wY -> q wY wZ -> r wX wZ) -> w p -> w q -> w r Source

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

Instances

Gap FreeRight
Gap FreeLeft