Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.SMonad

Contents

Transpose an SMonad with other constructors.

Description

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

Synopsis

class Monoid i => SMonad i m | m -> i where
- (>>+) :: m a -> (i -> a -> m b) -> m b
- enter :: i -> a -> m a
- exit :: m a -> a
(+<<) :: SMonad i m => (i -> a -> m b) -> m a -> m b
imap :: SMonad i m => (i -> a -> b) -> m a -> m b
pami :: SMonad i m => m a -> (i -> a -> b) -> m b
exitWith :: SMonad i m => (i -> a -> b) -> m a -> b
withExit :: SMonad i m => m a -> (i -> a -> b) -> b
iact :: (Monad m, SMonad i m) => i -> m a -> m a
newtype ViaSMonad m a = ViaSMonad {
- runViaSMonad :: m a
}
data XSuspend i a = Suspend i a
type XSwp s a = XSuspend (KPerm s) a
getSwp :: (Typeable s, Swappable a) => XSwp s a -> a
type XRes s a = XSuspend [KAtom s] a
getRes :: KRestrict s a => XRes s a -> a
transposeMF :: (Functor f, SMonad i m) => m (f a) -> f (m a)
transposeFM :: (Traversable f, Applicative m, SMonad i m) => f (m a) -> m (f a)

Documentation

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

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

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

enter :: i -> a -> m a Source #

Enter the suspended environment, by suspending i on a.

exit :: m a -> a Source #

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) Source #
Instance details Defined in Language.Nominal.SMonad Methods (>>+) :: XSuspend i a -> (i -> a -> XSuspend i b) -> XSuspend i b Source # enter :: i -> a -> XSuspend i a Source # exit :: XSuspend i a -> a Source #
SMonad [KAtom s] (KNom s) Source #
Instance details Defined in Language.Nominal.Nom Methods (>>+) :: KNom s a -> ([KAtom s] -> a -> KNom s b) -> KNom s b Source # enter :: [KAtom s] -> a -> KNom s a Source # exit :: KNom s a -> a Source #

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

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

An equivalent to fmap, with access to the monoid.

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

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

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

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

flip exitWith

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

An SMonad has an i-monoid action

newtype ViaSMonad m a Source #

Constructors

ViaSMonad
Fields runViaSMonad :: m a

Instances

SMonad i m => Monad (ViaSMonad m) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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 Source #

A generic type for suspended monoid operations

Constructors

Suspend i a

Instances

Monoid i => SMonad i (XSuspend i) Source #
Instance details Defined in Language.Nominal.SMonad Methods (>>+) :: XSuspend i a -> (i -> a -> XSuspend i b) -> XSuspend i b Source # enter :: i -> a -> XSuspend i a Source # exit :: XSuspend i a -> a Source #
Monoid i => Monad (XSuspend i) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details 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) Source #
Instance details Defined in Language.Nominal.SMonad Methods kswp :: Typeable s => KAtom s -> KAtom s -> XSuspend i a -> XSuspend i a Source #
type Rep (XSuspend i a) Source #
Instance details Defined in Language.Nominal.SMonad type Rep (XSuspend i a) = D1 (MetaData "XSuspend" "Language.Nominal.SMonad" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" 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 Source #

A type for suspended swappings

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

Exit with a swapping action, if available

type XRes s a = XSuspend [KAtom s] a Source #

A type for suspended restrictions

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

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) Source #

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) Source #

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

Documentation

Transpose an SMonad with other constructors.

Transpose an `SMonad` with other constructors.