Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Invertible p wX wY
- mkInvertible :: p wX wY -> Invertible p wX wY
- fromPositiveInvertible :: Invertible p wX wY -> p wX wY
- withInvertible :: (forall wA wB. p wA wB -> r) -> Invertible p wX wY -> r
Documentation
data Invertible p wX wY Source #
Wrapper type to allow formal inversion of patches which aren't really invertible.
Instances
mkInvertible :: p wX wY -> Invertible p wX wY Source #
Wrap a patch to make it (formally) Invertible
. The result is initially
positive i.e. Fwd
.
fromPositiveInvertible :: Invertible p wX wY -> p wX wY Source #
Get the underlying patch from an Invertible
, assuming (as a precondition)
that it is positive i.e. Fwd
.
withInvertible :: (forall wA wB. p wA wB -> r) -> Invertible p wX wY -> r Source #
Run a function on the patch inside an Invertible
. The function has to be
parametric in the witnesses, so we can run it with both a Fwd
and a Rev
patch.