| Safe Haskell | Safe-Infered |
|---|
Darcs.Witnesses.Sealed
- data Sealed a where
- seal :: a wX -> Sealed a
- unseal :: (forall wX. a wX -> b) -> Sealed a -> b
- mapSeal :: (forall wX. a wX -> b wX) -> Sealed a -> Sealed b
- unsafeUnseal :: Sealed a -> a wX
- unsafeUnsealFlipped :: FlippedSeal a wY -> a wX wY
- unsafeUnseal2 :: Sealed2 a -> a wX wY
- data Sealed2 a where
- seal2 :: a wX wY -> Sealed2 a
- unseal2 :: (forall wX wY. a wX wY -> b) -> Sealed2 a -> b
- mapSeal2 :: (forall wX wY. a wX wY -> b wX wY) -> Sealed2 a -> Sealed2 b
- data FlippedSeal a wY where
- FlippedSeal :: !(a wX wY) -> FlippedSeal a wY
- flipSeal :: a wX wY -> FlippedSeal a wY
- unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b
- mapFlipped :: (forall wX. a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ
- unsealM :: Monad m => m (Sealed a) -> (forall wX. a wX -> m b) -> m b
- liftSM :: Monad m => (forall wX. a wX -> b) -> m (Sealed a) -> m b
- class Gap w where
- data FreeLeft p
- unFreeLeft :: FreeLeft p -> Sealed (p wX)
- data FreeRight p
- unFreeRight :: FreeRight p -> FlippedSeal p wX
Documentation
data Sealed a where
unsafeUnseal :: Sealed a -> a wX
unsafeUnsealFlipped :: FlippedSeal a wY -> a wX wY
unsafeUnseal2 :: Sealed2 a -> a wX wY
data Sealed2 a where
data FlippedSeal a wY where
Constructors
| FlippedSeal :: !(a wX wY) -> FlippedSeal a wY |
flipSeal :: a wX wY -> FlippedSeal a wY
unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b
mapFlipped :: (forall wX. a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ
class Gap w where
Methods
emptyGap :: (forall wX. p wX wX) -> w p
An empty Gap, e.g. NilFL or NilRL
freeGap :: (forall wX wY. p wX wY) -> w p
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
Compose two Gap values together in series, e.g. 'joinGap (+>+)' or 'joinGap (:>:)'
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.
unFreeLeft :: FreeLeft p -> Sealed (p wX)
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.
unFreeRight :: FreeRight p -> FlippedSeal p wX
Unwrap a FreeRight value