Language.Nominal.SMonad

Typeclass and instances for a "suspended" monoid action. Three examples will be of particular interest:

• Suspend a permutation (XSwp s). (This is familiar from the theory of nominal rewriting, where swappings suspend on unknowns.)
• Suspend a binding (XRes s; we use this to define KNom).
• Suspend a capture-avoiding binding (KNom s).

Intuitively, KNom is just XRes plus Swappable plus IO (for fresh IDs).

Documentation

class Monoid i => SMonad i m | m -> i where

A typeclass for computing under a monoid action.

RULES:

exit . enter mempty ==  id
flip >>+ . const    ==  >==     i.e.   a' >>= f = a' >>+ const f
enter mempty        ==  return

In other words:

• +<< . const and enter mempty form a monad.
• enter mempty followed by exit is a noop.

Methods

(>>+) :: m a -> (i -> a -> m b) -> m b

Move from one suspended environment to another via a function i -> a -> m b.

enter :: i -> a -> m a

Enter the suspended environment, by suspending i on a.

exit :: m a -> a

Exit the suspended environment, discarding any suspended actions. Use exitWith to exit while folding actions into the computation.

Instances

Monoid i => SMonad i (XSuspend i)

Defined in Language.Nominal.SMonad

Methods

(>>+) :: XSuspend i a -> (i -> a -> XSuspend i b) -> XSuspend i b

enter :: i -> a -> XSuspend i a

exit :: XSuspend i a -> a

SMonad [KAtom s] (KNom s)

Defined in Language.Nominal.Nom

Methods

(>>+) :: KNom s a -> ([KAtom s] -> a -> KNom s b) -> KNom s b

enter :: [KAtom s] -> a -> KNom s a

exit :: KNom s a -> a

(+<<) :: SMonad i m => (i -> a -> m b) -> m a -> m b

imap :: SMonad i m => (i -> a -> b) -> m a -> m b

An equivalent to fmap, with access to the monoid.

pami :: SMonad i m => m a -> (i -> a -> b) -> m b

An equivalent to <&>, with access to the monoid.

exitWith :: SMonad i m => (i -> a -> b) -> m a -> b

Exit the SMonad, with a function to fold the monoid into the computation. So:

exit = exitWith (,)

withExit :: SMonad i m => m a -> (i -> a -> b) -> b

flip exitWith

iact :: (Monad m, SMonad i m) => i -> m a -> m a

An SMonad has an i-monoid action

newtype ViaSMonad m a

Constructors

ViaSMonad

Fields

• runViaSMonad :: m a

Instances

SMonad i m => Monad (ViaSMonad m)

Defined in Language.Nominal.SMonad

Methods

(>>=) :: ViaSMonad m a -> (a -> ViaSMonad m b) -> ViaSMonad m b

(>>) :: ViaSMonad m a -> ViaSMonad m b -> ViaSMonad m b

return :: a -> ViaSMonad m a

fail :: String -> ViaSMonad m a

SMonad i m => Functor (ViaSMonad m)

Defined in Language.Nominal.SMonad

Methods

fmap :: (a -> b) -> ViaSMonad m a -> ViaSMonad m b

(<$) :: a -> ViaSMonad m b -> ViaSMonad m a

SMonad i m => Applicative (ViaSMonad m)

Defined in Language.Nominal.SMonad

Methods

pure :: a -> ViaSMonad m a

(<*>) :: ViaSMonad m (a -> b) -> ViaSMonad m a -> ViaSMonad m b

liftA2 :: (a -> b -> c) -> ViaSMonad m a -> ViaSMonad m b -> ViaSMonad m c

(*>) :: ViaSMonad m a -> ViaSMonad m b -> ViaSMonad m b

(<*) :: ViaSMonad m a -> ViaSMonad m b -> ViaSMonad m a

data XSuspend i a

A generic type for suspended monoid operations

Constructors

Suspend i a

Instances

Monoid i => SMonad i (XSuspend i)

Defined in Language.Nominal.SMonad

Methods

(>>+) :: XSuspend i a -> (i -> a -> XSuspend i b) -> XSuspend i b

enter :: i -> a -> XSuspend i a

exit :: XSuspend i a -> a

Monoid i => Monad (XSuspend i)

Defined in Language.Nominal.SMonad

Methods

(>>=) :: XSuspend i a -> (a -> XSuspend i b) -> XSuspend i b

(>>) :: XSuspend i a -> XSuspend i b -> XSuspend i b

return :: a -> XSuspend i a

fail :: String -> XSuspend i a

Monoid i => Functor (XSuspend i)

Defined in Language.Nominal.SMonad

Methods

fmap :: (a -> b) -> XSuspend i a -> XSuspend i b

(<$) :: a -> XSuspend i b -> XSuspend i a

Monoid i => Applicative (XSuspend i)

Defined in Language.Nominal.SMonad

Methods

pure :: a -> XSuspend i a

(<*>) :: XSuspend i (a -> b) -> XSuspend i a -> XSuspend i b

liftA2 :: (a -> b -> c) -> XSuspend i a -> XSuspend i b -> XSuspend i c

(*>) :: XSuspend i a -> XSuspend i b -> XSuspend i b

(<*) :: XSuspend i a -> XSuspend i b -> XSuspend i a

(Eq i, Eq a) => Eq (XSuspend i a)

Defined in Language.Nominal.SMonad

Methods

(==) :: XSuspend i a -> XSuspend i a -> Bool

(/=) :: XSuspend i a -> XSuspend i a -> Bool

(Show i, Show a) => Show (XSuspend i a)

Defined in Language.Nominal.SMonad

Methods

showsPrec :: Int -> XSuspend i a -> ShowS

show :: XSuspend i a -> String

showList :: [XSuspend i a] -> ShowS

Generic (XSuspend i a)

Defined in Language.Nominal.SMonad

Associated Types

type Rep (XSuspend i a) :: Type -> Type

Methods

from :: XSuspend i a -> Rep (XSuspend i a) x

to :: Rep (XSuspend i a) x -> XSuspend i a

(Swappable i, Swappable a) => Swappable (XSuspend i a)

Defined in Language.Nominal.SMonad

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> XSuspend i a -> XSuspend i a

type Rep (XSuspend i a)

Defined in Language.Nominal.SMonad

type Rep (XSuspend i a) = D1 (MetaData "XSuspend" "Language.Nominal.SMonad" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "Suspend" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 i) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 a)))

type XSwp s a = XSuspend (KPerm s) a

A type for suspended swappings

getSwp :: (Typeable s, Swappable a) => XSwp s a -> a

Exit with a swapping action, if available

type XRes s a = XSuspend [KAtom s] a

A type for suspended restrictions

getRes :: KRestrict s a => XRes s a -> a

Exit with a restriction action, if available

Transpose an SMonad with other constructors.

transposeMF :: (Functor f, SMonad i m) => m (f a) -> f (m a)

Transpose an SMonad with a Functor

Note: if m is instantiated to KNom s then note there is no capture-avoidance here; local bindings are just moved around. A stronger version (with correspondingly stronger typeclass assumptions) is in transposeNomF.

transposeFM :: (Traversable f, Applicative m, SMonad i m) => f (m a) -> m (f a)

This is just an instance of a more general principle, since f is Traversable and we assume m applicative.