Control.IMonad.Restrict

Restricted monads are a subset of indexed monads where the return value is restricted to a single index. They build on top of IMonad using the (:=) type constructor which restricts the index of the return value.

Restriction

The (:=) type constructor restricts the index that the return value inhabits.

returnR and (!>=) provide the restricted operations corresponding to returnI and (?>=). If returnI and (?>=) satisfy the monad laws, then so will returnR and (!>=):

returnR >!> f = f

f >!> returnR = f

(f >!> g) >!> h = f >!> (g >!> h)

The type synonym R rearranges the type variables of the restricted monad to match conventional notation.

data (a := i) j where

(a := i) represents a locked value of type a that you can only access at the index i.

V seals values of type a, restricting them to a single index i.

Constructors

V :: a -> (a := i) i

type R m i j a = m (a := j) i

An indexed monad where the final index, j, is 'R'estricted

returnR :: IMonad m => a -> m (a := i) i

A returnI that restricts the final index

(!>=) :: IMonad m => m (a := j) i -> (a -> m b j) -> m b i infixl 1

A flipped bindI that restricts the intermediate and final index. Called "angelic bind" in Conor McBride's paper. The type of this function has the following specialization:

(!>=) :: IMonad m => m (a := j) i -> (a -> m (b := k) j) -> m (b := k) i

Functions

Functions derived from returnR and (!>=)

fmapR :: IMonad m => (a -> b) -> m (a := j) i -> m (b := j) i

All restricted monads are ordinary functors

(<!>) :: IMonad m => (a -> b) -> m (a := j) i -> m (b := j) i

Infix fmapR

(<.>) :: IMonad m => m ((a -> b) := j) i -> m (a := k) j -> m (b := k) i

All restricted monads are restricted applicatives

(=<!) :: IMonad m => (a -> m b j) -> m (a := j) i -> m b i infixr 1

A bindI that restricts the intermediate and final index. The type of this function has the following specialization:

(=<!) :: IMonad m => (a -> m (b := k) j) -> m (a := j) i -> m (b := k) i

(!>) :: IMonad m => m (a := j) i -> m b j -> m b i infixl 1

Sequence two indexed monads. The type of this function has the following specialization:

(!>) :: IMonad m => m (a := j) i -> m (b := k) j -> m (b := k) i

(>!>) :: IMonad m => (a -> m (b := j) i) -> (b -> m c j) -> a -> m c i infixr 1

Composition of restricted Kleisli arrows

This is equivalent to (>>>) from Control.Category.

The type of this function has the following specialization:

IMonad m => (a -> m (b:= j) i) -> (b -> m (c := k) j) -> (a -> m (c := k) i)

(<!<) :: IMonad m => (b -> m c j) -> (a -> m (b := j) i) -> a -> m c i infixr 1

Composition of restricted Kleisli arrows

This is equivalent to (<<<) from Control.Category.

The type of this function has the following specialization:

(<!<) :: IMonad m => (b -> m (c := k) j) -> (a -> m (b := j) i) -> a -> m (c := k) i

joinR :: IMonad m => m (m a j := j) i -> m a i

joinR joins two monad layers into one. The type of this function has the following specialization:

joinR :: IMonad m => m (m (a := k) j := j) i -> m (a := k) i

voidR :: IMonad m => m (a := i) i -> m (() := i) i

Discard the result of evaluation

foreverR :: IMonad m => m (a := i) i -> m (b := j) i

foreverR repeats the action indefinitely

mapMR :: IMonad m => (a -> m (b := i) i) -> [a] -> m ([b] := i) i

"mapMR f" is equivalent to "sequenceR . map f"

mapMR_ :: IMonad m => (a -> m (b := i) i) -> [a] -> m (() := i) i

"mapMR_ f" is equivalent to "sequenceR_ . map f"

forMR :: IMonad m => [a] -> (a -> m (b := i) i) -> m ([b] := i) i

mapMR with its arguments flipped

forMR_ :: IMonad m => [a] -> (a -> m (b := i) i) -> m (() := i) i

mapMR_ with its arguments flipped

replicateMR :: IMonad m => Int -> m (a := i) i -> m ([a] := i) i

"replicateMR n m" performs m n times and collects the results

replicateMR_ :: IMonad m => Int -> m (a := i) i -> m (() := i) i

"replicateMR_ n m" performs m n times and ignores the results

sequenceR :: IMonad m => [m (a := i) i] -> m ([a] := i) i

Evaluate each action from left to right and collect the results

sequenceR_ :: IMonad m => [m (a := i) i] -> m (() := i) i

Evaluate each action from left to right and ignore the results

whenR :: IMonad m => Bool -> m (() := i) i -> m (() := i) i

"whenR p m" executes m if p is True

unlessR :: IMonad m => Bool -> m (() := i) i -> m (() := i) i

"unlessR p m" executes m if p is False

Interoperability

The following types and functions convert between ordinary monads and restricted monads.

Use u to convert an ordinary monad to a restricted monad so that it can be used within an indexed do block like so:

-- Both do blocks are indexed, using syntax rebinding from Control.IMonad.Do
do x <- indexedAction
   lift $ do
       y <- u $ ordinaryAction1 x
       u $ ordinaryAction2 x y

Use D to convert an index-preserving restricted monad into an ordinary monad so that it can be used within a normal do block.

-- An ordinary do block (i.e. without syntax rebinding from Control.IMonad.Do)
do x <- D $ indexPreservingAction
   D $ anotherIndexPreservingAction x

data U m a i where

The U type 'U'pgrades ordinary monads to restricted monads

Constructors

U :: {..} -> U m a i

Fields

• unU :: m (a i)

Instances

Monad m => IFunctor k k (U k * m)

Methods

fmapI :: (U k * m :-> a) b -> (k :-> f a) (f b)

Monad m => IMonad k (U k * m)

Methods

returnI :: a i -> m a i

bindI :: (U k * m :-> a) (m b) -> (U k * m :-> m a) (m b)

u :: Monad m => m a -> U m (a := i) i

u transforms an ordinary monad into a restricted monad

data D i m r

The D type 'D'owngrades index-preserving restricted monads to ordinary monads

Constructors

D

Fields

• unD :: m (r := i) i

Instances

IMonad k m => Monad (D k i m)

Methods

(>>=) :: D k i m a -> (a -> D k i m b) -> D k i m b

(>>) :: D k i m a -> D k i m b -> D k i m b

return :: a -> D k i m a

fail :: String -> D k i m a

IMonad k m => Functor (D k i m)

Methods

fmap :: (a -> b) -> D k i m a -> D k i m b

(<$) :: a -> D k i m b -> D k i m a

IMonad k m => Applicative (D k i m)

Methods

pure :: a -> D k i m a

(<*>) :: D k i m (a -> b) -> D k i m a -> D k i m b

(*>) :: D k i m a -> D k i m b -> D k i m b

(<*) :: D k i m a -> D k i m b -> D k i m a