Safe Haskell | None |
---|---|

Language | Haskell2010 |

- data Sealed a where
- seal :: a wX -> Sealed a
- data Sealed2 a where
- seal2 :: a wX wY -> Sealed2 a
- data FlippedSeal a wY where
- FlippedSeal :: !(a wX wY) -> FlippedSeal a wY

- flipSeal :: a wX wY -> FlippedSeal a wY
- unsafeUnseal :: Sealed a -> a wX
- unsafeUnsealFlipped :: FlippedSeal a wY -> a wX wY
- unsafeUnseal2 :: Sealed2 a -> a wX wY
- unseal :: (forall wX. a wX -> b) -> Sealed a -> b
- 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
- mapSeal :: (forall wX. a wX -> b wX) -> Sealed a -> Sealed b
- mapFlipped :: (forall wX. a wX wY -> b wX wZ) -> FlippedSeal a wY -> FlippedSeal b wZ
- 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
- unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b
- newtype Poly a = Poly {
- unPoly :: forall wX. a wX

- newtype Stepped f a wX = Stepped {
- unStepped :: f (a wX)

- newtype FreeLeft p = FLInternal (Poly (Stepped Sealed p))
- newtype FreeRight p = FRInternal (Poly (FlippedSeal p))
- unFreeLeft :: FreeLeft p -> Sealed (p wX)
- unFreeRight :: FreeRight p -> FlippedSeal p wX
- class Gap w where

# Documentation

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.

The same as `Sealed`

but for two parameters (wX and wY).

data FlippedSeal a wY where Source

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

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

unsealFlipped :: (forall wX wY. a wX wY -> b) -> FlippedSeal a wZ -> b 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.

FLInternal (Poly (Stepped Sealed 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.

FRInternal (Poly (FlippedSeal p)) |

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

Unwrap a `FreeLeft`

value

unFreeRight :: FreeRight p -> FlippedSeal p wX Source

Unwrap a `FreeRight`

value

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 (:>:)'