Copyright | (c) 2012--2014 The University of Kansas |
---|---|

License | BSD3 |

Maintainer | Neil Sculthorpe <neil@ittc.ku.edu> |

Stability | beta |

Portability | ghc |

Safe Haskell | Safe-Inferred |

Language | Haskell2010 |

This module provides a type class for injective functions (and their projections),
and some useful interactions with `Transform`

.

- class Injection a u where
- injectM :: (Monad m, Injection a u) => a -> m u
- projectM :: (Monad m, Injection a u) => u -> m a
- projectWithFailMsgM :: (Monad m, Injection a u) => String -> u -> m a
- injectT :: (Monad m, Injection a u) => Transform c m a u
- projectT :: (Monad 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 :: (Monad m, Injection a u) => Transform c m a b -> Transform c m u b
- projectWithFailMsgT :: (Monad m, Injection a u) => String -> Transform c m u a
- promoteWithFailMsgT :: (Monad m, Injection a u) => String -> Transform c m a b -> Transform c m u b
- extractR :: (Monad m, Injection a u) => Rewrite c m u -> Rewrite c m a
- promoteR :: (Monad m, Injection a u) => Rewrite c m a -> Rewrite c m u
- extractWithFailMsgR :: (Monad m, Injection a u) => String -> Rewrite c m u -> Rewrite c m a
- promoteWithFailMsgR :: (Monad 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 :: (Monad m, Injection a u) => u -> m a Source

Projects a value and lifts it into a `Monad`

, with the possibility of failure.

projectWithFailMsgM :: (Monad 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 :: (Monad 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 :: (Monad 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 :: (Monad 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 :: (Monad 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 :: (Monad 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).