Language.KURE.Injection

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

Injection Class

class Injection a u where

A class of injective functions from a to b, and their projections. The following law is expected to hold:

project (inject a) == Just a

Methods

inject :: a -> u

project :: u -> Maybe a

Instances

Injection a a

There is an identity injection for all types.

Defined in Language.KURE.Injection

Methods

inject :: a -> a

project :: a -> Maybe a

Injection a (Maybe a)

Defined in Language.KURE.Injection

Methods

inject :: a -> Maybe a

project :: Maybe a -> Maybe a

Monad Injections

injectM :: (Monad m, Injection a u) => a -> m u

Injects a value and lifts it into a Monad.

projectM :: (MonadFail m, Injection a u) => u -> m a

Projects a value and lifts it into a Monad, with the possibility of failure.

projectWithFailMsgM :: (MonadFail m, Injection a u) => String -> u -> m a

As projectM, but takes a custom error message to use if projection fails.

Transformation Injections

injectT :: (Monad m, Injection a u) => Transform c m a u

Lifted inject.

projectT :: (MonadFail m, Injection a u) => Transform c m u a

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

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

Promote a transformation over a value into a transformation over an injection of that value, (failing if that injected value cannot be projected).

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

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

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

Promote a rewrite over a value into a rewrite over an injection of that value, (failing if that injected value cannot be projected).

extractWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m u -> Rewrite c m a

As extractR, but takes a custom error message to use if extraction fails.

promoteWithFailMsgR :: (MonadFail m, Injection a u) => String -> Rewrite c m a -> Rewrite c m u

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