Safe Haskell | None |
---|---|
Language | Haskell98 |
Darcs.Witnesses.Sealed
- data Sealed a where
- 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
- 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
- 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
- data FreeLeft p
- unFreeLeft :: FreeLeft p -> Sealed (p x)
- data FreeRight p
- unFreeRight :: FreeRight p -> FlippedSeal p x
Documentation
unsafeUnseal :: Sealed a -> a x Source
unsafeUnsealFlipped :: FlippedSeal a y -> a x y Source
unsafeUnseal2 :: Sealed2 a -> a x y 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
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 (:>:)'
'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 x) Source
Unwrap a FreeLeft
value
'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 x Source
Unwrap a FreeRight
value