Language.KURE.Injection

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

A particularly useful instance of Injection is from a to Generic a, and that case is the primary purpose of most of these combinators.

Injection Class

class Injection a b where

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

 retract (inject a) == Just a

Methods

inject :: a -> b

retract :: b -> Maybe a

Instances

Injection a a

There is an identity injection for all types.

Injection a (Maybe a)

Monad Injections

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

Injects a value and lifts it into a Monad.

retractM :: (MonadPlus m, Injection a a') => a' -> m a

Retracts a value and lifts it into a MonadPlus, producing mzero if the retraction fails.

Translate Injections

injectT :: (Monad m, Injection a a') => Translate c m a a'

Lifted inject.

retractT :: (MonadPlus m, Injection a a') => Translate c m a' a

Lifted retract, the Translate fails if the retraction fails.

extractT :: (Monad m, Injection a a') => Translate c m a' b -> Translate c m a b

Convert a Translate over an injected value into a Translate over a non-injected value.

promoteT :: (MonadPlus m, Injection a a') => Translate c m a b -> Translate c m a' b

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

extractR :: (MonadPlus m, Injection a a') => Rewrite c m a' -> Rewrite c m a

Convert a Rewrite over an injected value into a Rewrite over a retraction of that value, (failing if that injected value cannot be retracted).

promoteR :: (MonadPlus m, Injection a a') => Rewrite c m a -> Rewrite c m a'

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

Lens Injections

injectL :: (MonadPlus m, Injection a a') => Lens c m a a'

A Lens to the injection of a value.

retractL :: (MonadPlus m, Injection a a') => Lens c m a' a

A Lens to the retraction of a value.