nom-0.1.0.2: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

Language.Nominal.SMonad

Contents

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

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 #

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

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