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 `Translate`

.

- 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) => Translate c m a g
- projectT :: (Monad m, Injection a g) => Translate c m g a
- extractT :: (Monad m, Injection a g) => Translate c m g b -> Translate c m a b
- promoteT :: (Monad m, Injection a g) => Translate c m a b -> Translate c m g b
- promoteWithFailMsgT :: (Monad m, Injection a g) => String -> Translate c m a b -> Translate 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.

# Translate Injections

promoteWithFailMsgT :: (Monad m, Injection a g) => String -> Translate c m a b -> Translate c m g bSource

As `promoteT`

, but takes a custom error message to use if promotion fails.