Portability | ghc |
---|---|
Stability | beta |
Maintainer | Neil Sculthorpe <neil@ittc.ku.edu> |
Safe Haskell | Safe-Inferred |
This module provides a type class for injective functions (and their projections),
and some useful interactions with Transform
.
- class Injection a b where
- injectM :: (Monad m, Injection a g) => a -> m g
- projectM :: (Monad m, Injection a g) => g -> m a
- projectWithFailMsgM :: (Monad m, Injection a g) => String -> g -> m a
- injectT :: (Monad m, Injection a g) => Transform c m a g
- projectT :: (Monad m, Injection a g) => Transform c m g a
- extractT :: (Monad m, Injection a g) => Transform c m g b -> Transform c m a b
- promoteT :: (Monad m, Injection a g) => Transform c m a b -> Transform c m g b
- promoteWithFailMsgT :: (Monad m, Injection a g) => String -> Transform c m a b -> Transform c m g b
- extractR :: (Monad m, Injection a g) => Rewrite c m g -> Rewrite c m a
- promoteR :: (Monad m, Injection a g) => Rewrite c m a -> Rewrite c m g
- extractWithFailMsgR :: (Monad m, Injection a g) => String -> Rewrite c m g -> Rewrite c m a
- promoteWithFailMsgR :: (Monad m, Injection a g) => String -> Rewrite c m a -> Rewrite c m g
Injection Class
class Injection a b whereSource
A class of injective functions from a
to b
, and their projections.
The following law is expected to hold:
project (inject a) == Just a
Monad Injections
projectM :: (Monad m, Injection a g) => g -> m aSource
Projects a value and lifts it into a Monad
, with the possibility of failure.
projectWithFailMsgM :: (Monad m, Injection a g) => String -> g -> m aSource
As projectM
, but takes a custom error message to use if projection fails.
Transformation Injections
projectT :: (Monad m, Injection a g) => Transform c m g aSource
Lifted project
, the transformation fails if the projection fails.
extractT :: (Monad m, Injection a g) => Transform c m g b -> Transform c m a bSource
Convert a transformation over an injected value into a transformation over a non-injected value.
promoteT :: (Monad m, Injection a g) => Transform c m a b -> Transform c m g bSource
Promote a transformation over a value into a transformation over an injection of that value, (failing if that injected value cannot be projected).
promoteWithFailMsgT :: (Monad m, Injection a g) => String -> Transform c m a b -> Transform c m g bSource
As promoteT
, but takes a custom error message to use if promotion fails.
Rewrite Injections
extractR :: (Monad m, Injection a g) => Rewrite c m g -> Rewrite c m aSource
Convert a rewrite over an injected value into a rewrite over a projection of that value, (failing if that injected value cannot be projected).
promoteR :: (Monad m, Injection a g) => Rewrite c m a -> Rewrite c m gSource
Promote a rewrite over a value into a rewrite over an injection of that value, (failing if that injected value cannot be projected).