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

Safe Haskell | None

Darcs.Witnesses.Sealed

Synopsis

- data Sealed a where
  - Sealed :: a x -> Sealed a
- 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
  - Sealed2 :: !(a x y) -> Sealed2 a
- 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
  - emptyGap :: (forall x. p x x) -> w p
  - freeGap :: (forall x y. p x y) -> w p
  - joinGap :: (forall x y z. p x y -> q y z -> r x z) -> w p -> w q -> w r
- data FreeLeft p
- unFreeLeft :: FreeLeft p -> Sealed (p x)
- data FreeRight p
- unFreeRight :: FreeRight p -> FlippedSeal p x

# Documentation

data Sealed a where

Constructors

Sealed :: a x -> Sealed a |

Instances

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

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

Constructors

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

Instances

Show2 a => Show (Sealed2 a) |

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

Constructors

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

`Gap` abstracts over `FreeLeft` and `FreeRight` for code constructing these values

Methods

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

An empty `Gap`, e.g. `NilFL` or `NilRL`

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

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

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

Instances

Gap FreeRight |
Gap FreeLeft |

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.

Instances

Gap FreeLeft |

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

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.

Instances

Gap FreeRight |

unFreeRight :: FreeRight p -> FlippedSeal p x

Unwrap a `FreeRight` value