Safe Haskell | Safe-Infered |
---|

- data (a := i) j where
- type R m i j a = m (a := j) i
- returnR :: IMonad m => a -> m (a := i) i
- (!>=) :: IMonad m => m (a := j) i -> (a -> m (b := k) j) -> m (b := k) i
- fmapR :: IMonad m => (a -> b) -> m (a := j) i -> m (b := j) i
- (<!>) :: IMonad m => (a -> b) -> m (a := j) i -> m (b := j) i
- (<.>) :: IMonad m => m ((a -> b) := j) i -> m (a := k) j -> m (b := k) i
- (=<!) :: IMonad m => (a -> m (b := k) j) -> m (a := j) i -> m (b := k) i
- (!>) :: IMonad m => m (a := j) i -> m (b := k) j -> m (b := k) i
- (>!>) :: IMonad m => (a -> m (b := j) i) -> (b -> m (c := k) j) -> a -> m (c := k) i
- (<!<) :: IMonad m => (b -> m (c := k) j) -> (a -> m (b := j) i) -> a -> m (c := k) i
- joinR :: IMonad m => m (m (a := k) j := j) i -> m (a := k) i
- voidR :: IMonad m => m (a := i) i -> m (() := i) i
- foreverR :: IMonad m => m (a := i) i -> m (b := j) i
- mapMR :: IMonad m => (a -> m (b := i) i) -> [a] -> m ([b] := i) i
- mapMR_ :: IMonad m => (a -> m (b := i) i) -> [a] -> m (() := i) i
- forMR :: IMonad m => [a] -> (a -> m (b := i) i) -> m ([b] := i) i
- forMR_ :: IMonad m => [a] -> (a -> m (b := i) i) -> m (() := i) i
- replicateMR :: IMonad m => Int -> m (a := i) i -> m ([a] := i) i
- replicateMR_ :: IMonad m => Int -> m (a := i) i -> m (() := i) i
- sequenceR :: IMonad m => [m (a := i) i] -> m ([a] := i) i
- sequenceR_ :: IMonad m => [m (a := i) i] -> m (() := i) i
- whenR :: IMonad m => Bool -> m (() := i) i -> m (() := i) i
- unlessR :: IMonad m => Bool -> m (() := i) i -> m (() := i) i
- data U m a i where
- u :: Monad m => m a -> U m (a := i) i
- data D i m r = D {}

# 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.

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

.

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

A flipped `bindI`

that restricts the intermediate and final index

# Functions

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

All restricted monads are ordinary functors

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

All restricted monads are restricted applicatives

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

A `bindI`

that restricts the intermediate and final index

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

Composition of restricted Kleisli arrows

This is equivalent to (`>>>`

) from `Control.Category`

.

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

Composition of restricted Kleisli arrows

This is equivalent to (`<<<`

) from `Control.Category`

.

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

`joinR`

joins two monad layers into one

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

"`mapMR f`

" is equivalent to "`sequenceR . map f`

"

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

"`mapMR_ f`

" is equivalent to "`sequenceR_ . map f`

"

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

`mapMR`

with its arguments flipped

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

`mapMR_`

with its arguments flipped

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

"`replicateMR n m`

" performs `m`

`n`

times and collects the results

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

"`replicateMR_ n m`

" performs `m`

`n`

times and ignores the results

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

Evaluate each action from left to right and collect the results

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

Evaluate each action from left to right and ignore the results

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

"`whenR p m`

" executes `m`

if `p`

is `True`

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

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

The `U`

type 'U'pgrades ordinary monads to restricted monads