kure-2.12.0: Combinators for Strategic Programming

Portabilityghc
Stabilitybeta
MaintainerNeil Sculthorpe <neil@ittc.ku.edu>
Safe HaskellSafe-Inferred

Language.KURE.Injection

Contents

Description

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

Synopsis

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

Methods

inject :: a -> bSource

project :: b -> Maybe aSource

Instances

Injection a a

There is an identity injection for all types.

Injection a (Maybe a) 

Monad Injections

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

Injects a value and lifts it into a Monad.

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

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

Lifted inject.

projectT :: (Monad m, Injection a g) => Translate c m g aSource

Lifted project, the Translate fails if the projection fails.

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

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

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

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

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.

Rewrite Injections

extractR :: (Monad m, Injection a g) => Rewrite c m g -> Rewrite c m aSource

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 g) => Rewrite c m a -> Rewrite c m gSource

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

extractWithFailMsgR :: (Monad m, Injection a g) => String -> Rewrite c m g -> Rewrite c m aSource

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

promoteWithFailMsgR :: (Monad m, Injection a g) => String -> Rewrite c m a -> Rewrite c m gSource

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