| Copyright | (c) 2012--2021 The University of Kansas |
|---|---|
| License | BSD3 |
| Maintainer | Neil Sculthorpe <neil.sculthorpe@ntu.ac.uk> |
| Stability | beta |
| Portability | ghc |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Language.KURE.Injection
Description
This module provides a type class for injective functions (and their projections),
and some useful interactions with Transform.
Synopsis
- class Injection a u where
- injectM :: (Monad m, Injection a u) => a -> m u
- projectM :: (MonadFail m, Injection a u) => u -> m a
- projectWithFailMsgM :: (MonadFail m, Injection a u) => String -> u -> m a
- injectT :: (Monad m, Injection a u) => Transform c m a u
- projectT :: (MonadFail m, Injection a u) => Transform c m u a
- extractT :: (Monad m, Injection a u) => Transform c m u b -> Transform c m a b
- promoteT :: (MonadFail m, Injection a u) => Transform c m a b -> Transform c m u b
- projectWithFailMsgT :: (MonadFail m, Injection a u) => String -> Transform c m u a
- promoteWithFailMsgT :: (MonadFail m, Injection a u) => String -> Transform c m a b -> Transform c m u b
- extractR :: (MonadFail m, Injection a u) => Rewrite c m u -> Rewrite c m a
- promoteR :: (MonadFail m, Injection a u) => Rewrite c m a -> Rewrite c m u
- extractWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m u -> Rewrite c m a
- promoteWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m a -> Rewrite c m u
Injection Class
class Injection a u where Source #
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 :: (MonadFail m, Injection a u) => u -> m a Source #
Projects a value and lifts it into a Monad, with the possibility of failure.
projectWithFailMsgM :: (MonadFail m, Injection a u) => String -> u -> m a Source #
As projectM, but takes a custom error message to use if projection fails.
Transformation Injections
projectT :: (MonadFail m, Injection a u) => Transform c m u a Source #
Lifted project, the transformation fails if the projection fails.
extractT :: (Monad m, Injection a u) => Transform c m u b -> Transform c m a b Source #
Convert a transformation over an injected value into a transformation over a non-injected value.
promoteT :: (MonadFail m, Injection a u) => Transform c m a b -> Transform c m u b Source #
Promote a transformation over a value into a transformation over an injection of that value, (failing if that injected value cannot be projected).
promoteWithFailMsgT :: (MonadFail m, Injection a u) => String -> Transform c m a b -> Transform c m u b Source #
As promoteT, but takes a custom error message to use if promotion fails.
Rewrite Injections
extractR :: (MonadFail m, Injection a u) => Rewrite c m u -> Rewrite c m a Source #
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 :: (MonadFail m, Injection a u) => Rewrite c m a -> Rewrite c m u Source #
Promote a rewrite over a value into a rewrite over an injection of that value, (failing if that injected value cannot be projected).