This file is |as-full.lgs|, the final version of an
action semantics~\cite{Mosses92:Action} implementation in a
\emph{modular} monadic semantics~\cite{Liang*95:Monad},
using resumptions for parallelism and with the addition of a
continuational facet.

\ifstandalone
\bibliographystyle{alpha}
\fi

\bigskip

File created by Keith Wansbrough 1996-07-26; last modified 1997-02-18.
\TeX\ generated output on \datestamp.

\bigskip

This is a literate Gofer script.  Lines beginning with |>| are code,
lines beginning with |*| are code that has been commented out, and all
other lines are commentary on the program.

\section*{History}

\begin{description}
\item[1996-07-26:] File creation.
\item[\dots]
\item[1997-02-18:] Final code tidy-up for thesis.
\end{description}

\section*{Known bugs}

\begin{itemize}
\item The communicative facet is extremely cut-down and bears little
  relation to Mosses' generalised system supporting multiple concurrent
  agents.
  Also, |yCurrentBuffer| (i.e., |getbufC|) blocks while waiting for
  input, blocking all other threads.
\item I don't check if something is bindable or storable before binding
  it or storing it.  Note especially that an attempt to bind or store
  |tnil| should cause the action to fail.
\item |getTransient| currently only reads non-digit-separated non-negative
  integers (in |commToIO|, Section~\ref{sec:code:communications}).
\item Lifting of |NondetMMonad| through |ContT|
  (Section~\ref{sec:code:list-monad-transformer}) involves duplicating a
  continuation, which is probably illegal.
\item A number of actions, combinators and yielders give run-time type
  errors (with |prj1'|) if passed an incorrect type, rather than failing
  (for actions and combinators) or yielding |tnil| (for yielders).
\end{itemize}

\section*{To do}

Nothing.


\ifstandalone
\tableofcontents
\fi

\section*{Naming conventions}

The following naming conventions are followed throughout the code.  They
have been influenced by the Hungarian notation~\cite{Simonyi*91:Hungarian}
often used by Windows programmers.

\begin{itemize}
\item Actions are represented by names beginning with |a|: |aGive|,
  |aChoose|, |aBindTo| etc.
\item Combinators are represented by names beginning with |c|: |cAnd|,
  |cHence|, |cAndThenMoreover| etc.
\item Yielders are represented by names beginning with |y|: |yIt|,
  |yDataBoundTo|, |yReceiving| etc.
\item Data operations, as yielders, also have names beginning with |y|:
  |yCount|, |yPredecessorOf| etc.  But data operations are built from
  operations on data, which have the same name but with a trailing
  underscore: |yCount_|, |yPredecessorOf_|.
\item The basic operators of monads of type |MMonad| are tagged with a
  trailing |M|: |unitM|, |bindM| and |runM|.
\item The `levels' built into the action monad are represented by
  the tags $B$ for |Behaviour| (and sometimes also for the
  |(Behaviour,Commitment)| tuple known as |State| or action state),
  $A$ for actions and abstractions of actions (especially the abstraction
  stored for |cUnfolding|\dots|aUnfold|),
  $X$ for |Commitment|,
  $E$ for |Environment|,
  $S$ for |Store|,
  $C$ for |Communication|,
  $D$ for |Redirection|,
  $K$ for continuations,
  $N$ for nondeterminism,
  $R$ for resumptions,
  and $P$ for parallelism.
\item These level tags appear in several places.  The names of the
  accessor operators have the tag as a capital letter appended to their
  names: |doB|, |unX|, |setE| etc.  The local variables used to store
  these values in the definitions of the accessors and elsewhere are the
  lower-case tag, sometimes with a suffix digit or prime: |b|, |e0|,
  |s'| etc.
\item Local variables (i.e., variables with scope of only a few lines):
  |t| for a |Transient| (i.e., a data value); |f| for an auxiliary
  function; |y| for a yielder.  These can have suffixes: |t1|, |t2|, for
  example, or |yt| for a yielder that yields a transient, |ye| for a
  yielder that yields an environment.
\item Following the \textsc{Lisp} convention, a suffix |_p| means that
  the function is a predicate: it returns a |Bool|.
\item As is standard Gofer/Haskell practice, in list pattern matching
  |x| is a generic list element, and |xs| is a list of |x|s.  So |(x:xs)|
  matches the head and tail of a non-empty list.
\end{itemize}


\section{Preliminaries}
\label{sec:code:preliminaries}

\subsection{Extensible union types}
\label{sec:code:extensible-union-types}

First we define a system of extensible union types, to be used for the
domains of our semantics.  This system is that used by Liang, Hudak and
Jones in their paper~\cite{Liang*95:Monad}.  Unfortunately, the
definition of |SubType| requires class types with two arguments, which
are a Gofer-specific feature not found in Haskell (at least to version
1.3~\cite[p.~40]{Peterson*96:Report}).

First, |OR|, which forms the disjoint (tagged) union of two types.

> data OR a b = L a | R b

> instance (Text a, Text b) => Text (OR a b) where
>   showsPrec n (L l) = showsPrec n l
>   showsPrec n (R r) = showsPrec n r

> instance (Eq a, Eq b) => Eq (OR a b) where
>   L a1 == L a2  =  a1 == a2
>   R b1 == R b2  =  b1 == b2
>   _    == _     =  False

Now |Maybe|, which represents an optional value: either data or nothing.

> data Maybe a = Just a | Nothing

> instance Eq a => Eq (Maybe a) where
>   Just x  == Just y   =  x == y
>   Nothing == Nothing  =  True
>   _       == _        =  False

The class |SubType| is Liang, Hudak and Jones'~\cite{Liang*95:Monad}
crucial use of the Gofer class system.  It allows us to state that one
type is the direct subtype of another, and to give injection and
projection functions relating the two types.  The Gofer type system will
then automatically compose the series of injections or projections
required to relate any two types related by the (transitive) subtype
relation.

Our addition to Liang, Hudak and Jones' definition is |prj1|, which
forces the projection; if it fails it throws a run-time type error.  We
also have |prj1'|, which is identical but gives a specific error
(useful for tracing type errors!).

> class SubType sub sup where
>   inj   :: sub -> sup
>   prj   :: sup -> Maybe sub
>   prj1  :: sup -> sub
>   prj1' :: sup -> String -> sub

>   prj1 x    = case prj x of
>                 Just x' -> x'
>                 Nothing -> error "run-time type error"
>   prj1' x s = case prj x of
>                 Just x' -> x'
>                 Nothing -> error ("run-time type error: " ++ s)

|inj| injects an element of the subtype into the supertype; |prj|
projects an element of the supertype into the subtype if possible,
otherwise returns |Nothing|.  |prj1| and |prj1'| force the projection:
instead of returning a |Maybe| type, they return the value itself, or
exit with an error.

> instance SubType a (OR a b) where
>   inj        = L
>   prj (L x)  = Just x
>   prj _      = Nothing

> instance SubType a b => SubType a (OR c b) where
>   inj        = R . inj
>   prj (R a)  = prj a
>   prj _      = Nothing

We have a type |Bottom| that is just that.  It is used as the base type
of our extensible disjoint union, and is not intended to have any
values!

> data Bottom = Bottom

> instance Text Bottom where
>   showsPrec _ _ = error "attempt to show Bottom"

> instance Eq Bottom where
>   _ == _  =  error "attempt to compare Bottom for equality"


\subsection{Monads and monad transformers}
\label{sec:code:monads-and-monad-transformers}

\subsubsection{Monads}
\label{sec:code:monads}

So what's a monad?

> class MMonad m where
>   unitM :: a -> m a
>   bindM :: m a -> (a -> m b) -> m b
>   runM  :: m a -> IO a

|unitM a| places the value |a| into the monad.  |m1 `bindM` \v -> m2|
binds two monads together, passing the result of the first monad to the
second.  |runM m| `runs' a monad, converting it into an I/O monad
returning the same value.

\medskip

A very useful monad operation is |nop|, which returns the empty tuple
|()|.  We define it here, since all our monads should have it.

>   nop   :: m ()
>   nop   =  unitM ()

Note that this is |MMonad| (and |unitM|, |bindM|, |runM| etc.)\ to avoid
conflicts with the |Monad| declaration in the |cc| prelude.  We want to
explicitly define our monads in this file.

\medskip

As well as the above types, we have three proof
obligations~\cite{Wadler92:Essence}:
\begin{itemize}
\item |(unitM a) `bindM` k = k a|. \hfill(\emph{left unit})
\item |m `bindM` unitM = m|.\hfill(\emph{right unit})
\item |    m `bindM` (\a -> (k a) `bindM` (\b -> h b))|\\
      |=  (m `bindM` (\a -> k a)) `bindM` (\b -> h b)|.
      \hfill(\emph{associative})
\end{itemize}

\subsubsection{Monad transformers}
\label{sec:code:monad-transformers}

Monad transformers are type operations that tranform one monad into
another.

> class (MMonad m, MMonad (t m)) => MMonadT t m where
>   liftM  ::  m a                ->  t m a

A monad transformer |t| provides a function that lifts computations in |m|
to computations in |t m|.

\medskip

The proof obligations (\cite[p.~339]{Liang*95:Monad}) are:
\begin{itemize}
\item If |m| is a monad, then |t m| is a monad (i.e., satisfies the
monad laws given in Section~\ref{sec:code:monads}).
\item |liftM . unitM| = |unitM|.
\item |liftM (m `bindM` k)| = |liftM m `bindM` (liftM . k)|.
\end{itemize}


\section{Types}
\label{sec:code:types}

\subsection{Support types}
\label{sec:code:support-types}

First we define some support types for computation.

\subsubsection{Maps}
\label{sec:code:maps}

The |Map| type represents a map from one type to another.

> data Map a b = Map [(a,b)]

It's a list of pairs |(a,b)| mapping |a| to |b| (the first map |(a,_)|
in the list masks subsequent ones).  We use this system, rather
than a function from |a| to |Maybe b|, because we want to be able to
view the map and to examine the mapped set of the map.

> instance Text [(a,b)] => Text (Map a b) where
>   showsPrec n (Map xs) = showsPrec n xs

> instance Eq [(a,b)] => Eq (Map a b) where
>   Map e1 == Map e2  =  e1 == e2

This |==| is a bit harsh: it should really be at least |tidyMap ei| that
are compared, and even then the order should not matter.

> emptyMap   ::         Map a b
> mapTo      ::         a -> b -> Map a b
> mapOverlay ::         Map a b -> Map a b -> Map a b
> mappedTo   :: Eq a => Map a b -> a -> Maybe b
> mappedSet  ::         Map a b -> [a]
> mapMap     ::         ((a,b) -> (c,d)) -> Map a b -> Map c d
> unMap      :: Eq a => Map a b -> a -> Map a b
> tidyMap    :: Eq a => Map a b -> Map a b

|emptyMap| is the empty map.  |mapTo a b| returns the singleton map from
|a| to |b|.  |mapOverlay m1 m2| forms the union of maps |m1| and |m2|,
with mappings from |m2| taking precedence over mappings from |m1|.
|mappedTo m a| returns the value to which |a| is mapped, or nothing.
|mappedSet m| returns a list of all mapped values in |m|.  |mapMap|
allows us to map a function over a |Map|.  |unMap| deletes a mapping
from the map.  |tidyMap| tidies up a map by removing duplicate mappings,
without affecting the value of the map.

> emptyMap = Map []

> mapTo a b = Map [(a,b)]

> mapOverlay (Map m1) (Map m2) = Map (m2 ++ m1)

If you want |mapOverlay| to remove redundant entries, use the
following (but you'll need to add |Eq a =>| to the type):

* mapOverlay (Map m1) (Map m2) = tidyMap (Map (m2 ++ m1))

> mappedTo (Map ((a1,b1):abs)) a
>   = if a==a1 then Just b1
>              else mappedTo (Map abs) a
> mappedTo (Map [])            _
>   = Nothing

> mappedSet (Map m) = map fst m

> mapMap f (Map xs) = Map (map f xs)

> unMap (Map abs) dela = Map (filter (\(a,b) -> a/=dela) abs)

> tidyMap (Map abs) = Map (fstnub abs)
>   where
>     fstnub ((a,b):abs) = (a,b) : (filter ((/=a).fst)
>                                          (fstnub abs))
>     fstnub []          = []


\subsubsection{Empty types}
\label{sec:code:empty-types}

Action Semantics has a number of `empty types', which represent the
absence of data.  The most obvious is the empty tuple, \textsf{nothing},
but there are also \textsf{uninitialised} and \textsf{unknown}.

These are represented here by a datatype |Empty| with nullary
constructors corresponding to the above values.

> data Empty = UnInitialised | UnKnown

Note that |tnil| (see Section~\ref{sec:code:tuple-handling}) is used in this
program to represent \textsf{nothing}.

> instance Text Empty where
>   showsPrec _ UnInitialised = showString "<uninitialised>"
>   showsPrec _ UnKnown       = showString "<unknown>"

> instance Eq Empty where
>   UnInitialised == UnInitialised    =  True
>   UnKnown       == UnKnown          =  True
>   _             == _                =  False


\subsection{Facet types}
\label{sec:code:facet-types}

Now we define the types that are used for the action monad's facets.

\subsubsection{Behaviour}
\label{sec:code:behaviour}

> data Behaviour = Tr Transient | Esc Transient | Fail

The |Behaviour| exhibited by an action is either completion (with a
transient), escape (with a transient), or failure (or divergence, but
that is handled differently).  Note that we do not \emph{quite} follow
Mosses here with respect to environments.  See
Section~\ref{sec:code:actions-basic-and-functional}, |wipenev|, for how this
is handled.

> instance Eq Behaviour where
>   Tr  t1 == Tr  t2  =  t1 == t2
>   Esc t1 == Esc t2  =  t1 == t2
>   Fail   == Fail    =  True
>   _      == _       =  False

> instance Text Behaviour where
>   showsPrec n (Tr t)  = showString "Complete: " . showsPrec n t
>   showsPrec n (Esc t) = showString "Escape: " . showsPrec n t
>   showsPrec _ (Fail)  = showString "Fail"


\subsubsection{Commitment}
\label{sec:code:commitment}

> data Commitment = Com | Unc

The |Commitment| flag indicates whether
the action is |Com|\-mit\-ted or |Unc|om\-mit\-ted.

> instance Text Commitment where
>   showsPrec _ Com = showString "<committed>"
>   showsPrec _ Unc = showString "<uncommitted>"

> instance Eq Commitment where
>   Com == Com = True
>   Unc == Unc = True
>   _   == _   = False

|orCom| computes the logical `or' of its two arguments, which are
treated as booleans: |Com| is `true' and |Unc| is `false'.

> orCom :: Commitment -> Commitment -> Commitment

> x1 `orCom` x2 = if x1==Com || x2==Com then Com else Unc

> infixl `orCom`


\subsubsection{Action state}
\label{sec:code:action-state}

> data State = State Behaviour Commitment

The |State| is the
combination of the |Behaviour| and the |Commitment| flag.

> instance Text State where
>   showsPrec n (State b x) = showsPrec n b . 
>                             showString " " . showsPrec n x

\subsubsection{Environments}
\label{sec:code:environments}

Now we add in an environment.  With |Map| already defined, this is easy:
an environment is just a map from |Token| to |Transient|.

> type Token = String
> data Environment = Env (Map Token Transient)

> instance Text Token where
>   showsPrec _ s = showString s

> instance Text Environment where
>   showsPrec n (Env m) = showString "Env: " . showsPrec n m

> instance Eq Environment where
>   Env m1 == Env m2  =  m1 == m2

> emptyEnv   :: Environment
> bindTo     :: Token -> Transient -> Environment
> lookup     :: Token -> Environment -> Maybe Transient
> overlay    :: Environment -> Environment -> Environment
> isConflict :: Environment -> Environment -> Bool
> getEnvMap  :: Environment -> Map Transient Transient
> makeEnvMap :: Map Transient Transient -> Environment

|emptyEnv| is the empty environment.  
|bindTo| creates a binding between a |Token| and a |Transient|.
|lookup| finds the value associated with a |Token|, and
returns |Just|~$v$, or |Nothing| for failure.  |overlay| overlays its
first environment with its second.  |isConflict| returns |True| if the
two environments passed conflict (i.e., both contain bindings for some
token); |False| otherwise.  |getEnvMap|
converts an |Environment| into a map; |makeEnvMap| is its inverse.

> emptyEnv = Env emptyMap

> bindTo t v = Env (mapTo t v)

> lookup tok (Env m) = let v = mappedTo m tok in
>                        if v==Just unknown then Nothing
>                                           else v

> overlay (Env m1) (Env m2) = Env (mapOverlay m1 m2)

> isConflict (Env m1) (Env m2)
>   = not (null [ a | a <- mappedSet m1,
>            isBound m1 a,
>            isBound m2 a ] )
>   where isBound m2 a = case mappedTo m2 a of
>                          Just v  -> v /= unknown
>                          Nothing -> False

> getEnvMap (Env m) = mapMap (\(a,b) -> (inj a, b)) m

> makeEnvMap m
>   = Env (mapMap (\(a,b) -> (prj1' a "makeEnvMap", b)) m)


\subsubsection{Stores}
\label{sec:code:stores}

We need a \emph{store} to support level 4, the imperative facet.
Our access functions to the store vaguely resemble 
Liang, Hudak and Jones'~\cite{Liang*95:Monad} (which has
\emph{allocLoc}, \emph{lookupLoc} and \emph{updateLoc}; see Table~1 and
Section~5.3 of~\cite{Liang*95:Monad}).

> data Loc = Loc Int

We refer to cells by |Loc|.

> instance Text Loc where
>   showsPrec n (Loc loc) = showString "L" . showsPrec n loc

> instance Eq Loc where
>   (Loc x) == (Loc y) = x == y

> data Store = Store (Map Loc Transient) [Loc]

A |Store| is a map from |Loc| to |Transient|, followed by a `free list'
of unreserved cells.

> instance Text Store where
>   showsPrec n (Store m _) = showString "Store: " .
>                             showsPrec n (tidyMap m)

> emptyStore     :: Store
> uninitialised  :: Transient
> chooseFreeCell :: Store -> Loc
> reserveCell    :: Store -> Loc -> Maybe Store
> unreserveCell  :: Store -> Loc -> Maybe Store
> readCell       :: Store -> Loc -> Maybe Transient
> updateCell     :: Transient -> Store -> Loc -> Maybe Store
> getStoreMap    :: Store -> Map Transient Transient
> tidyStore      :: Store -> Store

|emptyStore| is an initial, empty store.
|uninitialised| is the value a cell holds until it has a value stored in
it. |chooseFreeCell| chooses a free cell, but \emph{does not remove it
from the free list}.
|reserveCell| reserves a cell in the store.  |unreserveCell|
frees a cell in the store.  |readCell| reads the
value of a given cell, and |updateCell| changes the value of a given
cell.  |getStoreMap| returns the |Map| representing the store.
|tidyStore| takes a store and tidies it up by removing all the duplicate
assignments to the same cell.  This does not affect the value of the
store, but cleans up some space.

|reserveCell|, |unreserveCell|, |readCell| and |updateCell| return
|Nothing| if they fail, or |Just foo| if they succeed.

> emptyStore = Store emptyMap (map Loc [1..])

> uninitialised = inj UnInitialised

> chooseFreeCell (Store _ (loc:_))
>     = loc
> chooseFreeCell (Store _ [])
>     = error "infinite memory ran out, sorry"

> reserveCell (Store m (locs)) loc
>     = case mappedTo m loc of
>         Nothing -> Just (Store (mapOverlay m
>                                   (mapTo loc uninitialised))
>                                (delfirst loc locs))
>         Just _  -> Nothing
>
>   where delfirst x (y:ys) | x==y       = ys
>                           | otherwise  = y : (delfirst x ys)

> unreserveCell (Store m locs) loc
>     = case mappedTo m loc of
>         Just _  -> Just (Store (unMap m loc) (loc:locs))
>         Nothing -> Nothing

> readCell (Store m _) loc
>     = mappedTo m loc

> updateCell t (Store m fl) loc
>     = case mappedTo m loc of
>         Just _  -> Just (Store (mapOverlay m (mapTo loc t)) fl)
>         Nothing -> Nothing

> getStoreMap (Store m _)
>     = mapMap (\(a,b) -> (inj a, b)) m

> tidyStore (Store m fl) = Store (tidyMap m) fl



\subsubsection{Abstractions}
\label{sec:code:abstractions}

Abstractions are simply actions, tagged with |Abstraction|.  Note that
these are used not only by the reflective facet, but also by the |UnfoldT|
transformer (Section~\ref{sec:code:bf-monad-transformer}) which implements
\textsf{unfolding}\dots\textsf{unfold}.

> data Abstraction = Abstraction Action

> instance Text Abstraction where
>   showsPrec _ (Abstraction _) = showString "<abstraction>"

You can't compare abstractions for equality:

> instance Eq Abstraction where
>   _ == _  =  False

The operations defined on |Abstraction|s are straightforward, and
trivially defined.

> abstractAct :: Action -> Abstraction
> enactAbs    :: Abstraction -> Action

|abstractAct| converts an action into an abstraction of that action;
|enactAbs| does the reverse, converting an abstraction into an action.

> abstractAct a = Abstraction a
> enactAbs (Abstraction a) = a


\subsubsection{Communications}
\label{sec:code:communications}

> type Communication = (RealWorld,Maybe Transient)

A |Communication| is a pair containing a |RealWorld| value (notionally
representing the state of the world, in reality merely for the purposes
of single-threading modifications to the world) and a buffer, which may
or may not contain an element of data.

Note that passing around a |RealWorld| value, as is done here, is only
possible due to some modifications I have made to Gofer to allow access
to it; I believe these modifications are necessary to construct an I/O
monad transformer.


\subsubsection{Redirections}
\label{sec:code:redirections}

An \emph{indirection} is basically a pointer: it enables us to create
circular or recursive bindings and data structures.  The set of
indirections (the redirection) looks very much like a store
(Section~\ref{sec:code:stores}).

> data Ind = Ind Int

We refer to individual indirections (internally) by |Ind|.

> instance Text Ind where
>   showsPrec n (Ind loc) = showString "P" . showsPrec n loc

> instance Eq Ind where
>   Ind x == Ind y  =  x == y

> data Redirection = Redirection (Map Ind Transient) [Ind]

A |Redirection| is a map from |Ind| to |Transient|, followed by a
`free list' of unused locations.

> instance Text Redirection where
>   showsPrec n (Redirection m _) = showString "Redirections: " .
>                                   showsPrec n (tidyMap m)

> emptyRedirection :: Redirection
> unknown      :: Transient
> makeInd      :: Redirection -> Transient
>                   -> Maybe (Redirection,Ind)
> redirInd     :: Redirection -> Ind -> Transient
>                   -> Maybe Redirection
> freeInd      :: Redirection -> Ind -> Maybe Redirection
> readInd      :: Ind -> Redirection -> Maybe Transient
> getRedirMap  :: Redirection -> Map Transient Transient
> makeRedirMap :: Map Transient Transient -> Redirection

|emptyRedirection| is the initial, empty redirection.  |unknown| is the
value given to an indirection that is not pointing anywhere.  |makeInd|
adds a new indirection to the redirection, pointing to the given
transient.  |redirInd| redirects the specified indirection to point to
the new transient.  |freeInd| frees the specified indirection.
|readInd| reads the value of the specified indirection.
|getRedirMap| gets a map of the current redirection;
|makeRedirMap| sets the current redirection to the given map.

|makeInd|, |redirInd|, |freeInd| and |readInd| return |Nothing| if they
fail, or |Just foo| if they succeed.

> emptyRedirection = Redirection emptyMap (map Ind [1..])

> unknown = inj UnKnown

> makeInd (Redirection m (loc:locs)) t
>     = Just (Redirection (mapOverlay m (mapTo loc t)) locs, loc)
> makeInd (Redirection _ []) _
>     = error "infinite indirection memory ran out, sorry"

> redirInd (Redirection m locs) loc t
>     = case mappedTo m loc of
>         Just _  -> Just (Redirection (mapOverlay m
>                                        (mapTo loc t)) locs)
>         Nothing -> Nothing

> freeInd (Redirection m locs) loc
>     = case mappedTo m loc of
>         Just _  -> Just (Redirection (unMap m loc) (loc:locs))
>         Nothing -> Nothing

> readInd loc (Redirection m _)
>     = mappedTo m loc

> getRedirMap (Redirection m _) = mapMap (\(a,b) -> (inj a, b)) m

> makeRedirMap m
>     = let m' = mapMap (\(a,b) -> (prj1' a "makeRedirMap", b)) m
>       in Redirection m' (map Ind [(firstFree m')..])
>   where firstFree = (1+) . maximum
>                          . map (\~(Ind n) -> n) . mappedSet

I know the above definition for |makeRedirMap| is ugly, but there would
seem to be no other easy way to determine the free list.  This method
may waste some storage, but works reasonably efficiently and well.



\subsection{The union type}
\label{sec:code:union-type}

\subsubsection{Definition}
\label{sec:code:definition}

Now we use the extensible disjoint union type mechanism to define
the type `|Transient|' as the union of a number of the other types we have
already defined.

> type TransientT
>   = OR [Transient]  -- must be at top  -- tuples
>    (OR Empty                           -- empty values
>    (OR Bool                            -- booleans
>    (OR Int                             -- integers
>    (OR (Map Transient Transient)       -- maps
>    (OR Token                           -- tokens
>    (OR Loc                             -- cells
>    (OR Abstraction                     -- abstractions
>    (OR Ind                             -- indirections
>        Bottom))))))))

> data Transient = Transient TransientT

> instance SubType a TransientT => SubType a Transient where
>   inj                = Transient . inj
>   prj (Transient x)  = prj x

A |Transient| is either an environment, a token, a tuple, an integer,
or a boolean.
There is a slight hack here because Gofer will not accept recursive
type synonyms; the hack is due to the writer (presumably Sheng Liang)
of |interp.gs| (Liang,
Hudak and Jones' sample modular monadic semantics code, available from
\path"ftp://nebula.cs.yale.edu/pub/yale-fp/modular-interpreter/"),
in the section entitled ``The Value Type'',
and it solves the problem for us fairly nicely.

> instance Text Transient where
>   showsPrec n (Transient x) = showsPrec n x

> instance Eq Transient where
>   Transient t1 == Transient t2 = t1 == t2


\subsubsection{Tuple handling}
\label{sec:code:tuple-handling}

Special handling is required to obtain the unusual semantics of Mosses'
tuples: they are \emph{not} normal lists
(see~\cite[\S E.2]{Mosses92:Action}).

> tnil  :: Transient
> tcons :: Transient -> Transient -> Transient

> tnil = inj ([]::[Transient])

|tnil| is the empty tuple; |tcons| takes two |Transient|s, possibly
tuples, and joins them together.  Note that tuple nesting is expressly
prohibited, and avoided by |tcons|: |tcons| is associative.  If |x| is a
non-tuple transient, it \emph{never} appears as |inj [x]|, but always as
a bare |inj x|.  This is what is ensured here: the result of
|tcons [] y| is |y|, not |[] ++ [y]| |= [y]|, etc.

> tcons x y = f (prj x) (prj y) where
>   f :: Maybe [Transient] -> Maybe [Transient] -> Transient
>   f (Just x') (Just y')  = inj (x' ++ y')
>   f (Just [])  Nothing   = y                -- x' == []
>   f (Just x')  Nothing   = inj (x' ++ [y])  -- x' /= []
>   f  Nothing  (Just [])  = x                -- y' == []
>   f  Nothing  (Just y')  = inj (x:y')       -- y' /= []
>   f  Nothing   Nothing   = inj (x:[y])

Next, we make lists of |a| a subtype of |[Transient]| if |a| is a
subtype of |Transient|.

> instance SubType a Transient
>     => SubType [a] [Transient] where
>   inj xs  = map inj xs
>   prj xs  = f (map prj xs) [] where
>               f (Just v  : xs') vs = f xs' (v:vs)
>               f (Nothing : _  ) vs = Nothing
>               f []              vs = Just (reverse vs)

In reality, |prj| will probably
either fail for the whole list or succeed for the whole list, so we
probably don't need to check every single element.  However, this was 
easy to code.

\medskip

And of course, lists of |Transient|s are a subtype of |Transient|.

> instance SubType [Transient] Transient where
>   inj [x]   = x
>   inj xs    = Transient (L xs)
>   prj (Transient (L xs)) = Just xs
>   prj x                  = Just [x]

This is a bit of a hack, and it relies on |[Transient]| being first in
the list of types in the union type.
Note that a singleton list becomes its element---this is in keeping with
Mosses.  In the opposite direction, anything other than a list is
projected onto a singleton list.


\subsubsection{Input and output}
\label{sec:code:input-and-output}

We here define two functions, |getTransient| and |putTransient|, that
allow us respectively to obtain a |Transient| from standard input and to
place a |Transient| on standard output, using Gofer's I/O monad
interface.

> getTransient :: IO Transient
> putTransient :: Transient -> IO ()

> getTransient = getTr0 []
>   where
>     getTr0 :: [Char] -> IO Transient
>     getTr0 cs = getchar `thenIO` \c ->
>                 if isDigit c
>                 then getTr0 (c:cs)
>                 else if null cs
>                      then getTr0 []
>                      else returnST (strToTransient cs)
>     strToTransient :: [Char] -> Transient
>     strToTransient ds = inj (g ds 0 1)
>     g :: [Char] -> Int -> Int -> Int
>     g (d:ds) n m = g ds (n + m * (ord d - ord '0')) (m * 10)
>     g []     n _ = n

> putTransient t = putString (show t ++ " ")

Note that |getTransient| currently only reads non-negative integers
delimited by non-digits.  |putTransient| however is general, since it
relies on the fact that |Transient| is an instance of |Text| and so
knows how to display itself.


\section{The action monad}
\label{sec:code:action-monad}

We define the monad that represents the various
facets of action semantics.  Since it is built from a base monad and
a series of monad transformers, we must define these first.

We must fulfill our proof obligations (see
Section~\ref{sec:code:monads-and-monad-transformers}) for each monad and
transformer.

\subsection{General monad transformers}
\label{sec:code:general-monad-transformers}

We build many of the specific monad transformers we need on the
following general monad transformers.  The code for these (|EnvT|
and |StateT|, and |ContT| later) is based on that found
in~\cite{Liang*95:Monad}.

Note that each monad transformer defines a monad class into which it
transforms monads.  These monad classes are defined here also, along
with the monad transformers themselves.

\subsubsection{Environment monad transformer}
\label{sec:code:environment-monad-transformer}

The environment monad transformer adds an environment to a monad: data
that can be read but not altered, but can be set to an arbitrary value
over a syntactically-limited scope.

The environment is represented by making the monad a function from the
passed-in environment to the resultant computation.

> data EnvT r m v = EVM (r -> m v)

> instance MMonad m => MMonad (EnvT r m) where
>   unitM v             = EVM (\_ -> unitM v)
>   ~(EVM m) `bindM` f  = EVM (\r -> m r           `bindM` \v ->
>                                    let EVM m2 = f v
>                                    in m2 r)
> --runM ~(EVM f)       = runM (f initialEnv)      `thenIO` \v ->
> --                      returnST v

Note that |runM| can't be specified in general, because we need to know
what |initialEnv| is.

> instance (MMonad m, MMonad (EnvT r m))
>               => MMonadT (EnvT r) m where
>   liftM m                      = EVM (\_ -> m)

> class MMonad m => EnvMMonad r m where
>   inEnv  ::  r -> m a -> m a
>   rdEnv  ::  m r

|EnvT| turns a monad into an |EnvMMonad|, with two operators. 
|inEnv r m| runs the monad |m| with its environment set to |r|.  |rdEnv|
accesses the value of the environment.

> instance MMonad m => EnvMMonad r (EnvT r m) where
>   inEnv r ~(EVM m) = EVM (\_ -> m r)
>   rdEnv            = EVM (\r -> unitM r)

|EnvMMonad|s must be lifted separately through each monad transformer,
as must all monads with operators taking monads as arguments.

> instance (EnvMMonad r m, MMonadT (EnvT r') m)
>               => EnvMMonad r (EnvT r' m) where
>   inEnv r ~(EVM m) = EVM (\r' -> inEnv r (m r'))
>   rdEnv            = liftM rdEnv

> instance (EnvMMonad r m, MMonadT (StateT s') m)
>               => EnvMMonad r (StateT s' m) where
>   inEnv r ~(STM m) = STM (\s' -> inEnv r (m s'))
>   rdEnv            = liftM rdEnv

> instance (EnvMMonad r m, MMonadT ListT m)
>               => EnvMMonad r (ListT m) where
>   inEnv r ~(LSM m) = LSM (inEnv r m)
>   rdEnv            = liftM rdEnv

> instance (EnvMMonad r m, MMonadT NondetT m)
>               => EnvMMonad r (NondetT m) where
>   inEnv r ~(NDM m) = NDM (\n' -> inEnv r (m n'))
>   rdEnv            = liftM rdEnv

> instance (EnvMMonad r m, MMonadT ResT m)
>               => EnvMMonad r (ResT m) where
>   inEnv r ~(RSM m) = RSM (inEnv r m)
>   rdEnv            = liftM rdEnv

> instance (EnvMMonad r m, MMonadT (ContT ans) m)
>               => EnvMMonad r (ContT ans m) where
>   inEnv r ~(CNM m) = CNM (\k' -> inEnv r (m k'))
>   rdEnv            = liftM rdEnv

Liang, Hudak and Jones~\cite[sec.~8.4]{Liang*95:Monad} claim that the above
is not the correct way of lifting |EnvMMonad| through |ContT|: ``an
interesting (but not natural)
way to lift |inEnv| is\dots''.  What they claim to be the correct
way to do it is below, commented out.

The above lifting has interesting consequences.  If the environment
transformer is inside the continuation transformer, then when the
continuation is invoked, whatever environment was in force at the time
of the invocation will remain, rather than being replaced by the
environment of the |call/cc|.  The `correct' version below takes special
care to always restore the environment.  But as with the lifting of
|callccK| through |StateT| in
Section~\ref{sec:code:continuation-monad-transformer}, we choose to expose
these effects of the sequence of composition, to allow the programmer
greater control (see~\cite{Steele94:Building}).

*   inEnv r ~(CNM m)
*     = CNM (\k' -> rdEnv                          `bindM` \r0 ->
*                   inEnv r (m (inEnv (r0 `asTypeOf` r) . k')))


\subsubsection{State monad transformer}
\label{sec:code:state-monad-transformer}

The state monad transformer adds state to a monad: data that can be read
or written arbitrarily.

The state is represented by making the monad a function from the
passed-in state to a computation of a pair of the resulting value and
the resulting state.

> data StateT s m v = STM (s -> m (v,s))

> instance MMonad m => MMonad (StateT s m) where
>   unitM v            = STM (\s -> unitM (v,s))
>   ~(STM m) `bindM` f = STM (\s -> m s        `bindM` \(v,s') ->
>                                   let STM m2 = f v
>                                   in m2 s')
> --runM ~(STM f)      = runM (f initialState) `thenIO` \(v,s) ->
> --                     returnST v

Note that |runM| can't be specified in general, because we need to know
what |initialState| is.

> instance (MMonad m, MMonad (StateT s m))
>               => MMonadT (StateT s) m where
>   liftM m = STM (\s -> m             `bindM` \v ->
>                        unitM (v,s))

> class MMonad m => StateMMonad s m where
>   getState :: m s
>   setState :: s -> m ()

|StateT| turns a monad into a |StateMMonad|, with two operators.
|getState| reads the current state, and |setState s| sets the current
state.

> instance MMonad m => StateMMonad s (StateT s m) where
>   getState   = STM (\s -> unitM (s ,s))
>   setState s = STM (\_ -> unitM ((),s))

|StateMMonad|s are readily lifted through any monad transformer:

> instance (StateMMonad s m, MMonadT t m)
>               => StateMMonad s (t m) where
>   getState   = liftM getState
>   setState s = liftM (setState s)


\subsection{The base monad}
\label{sec:code:base-monad}

The base monad has no features at all; it merely passes around values.

> data Id a = Id a

> instance MMonad Id where
>   unitM a           = Id a
>   ~(Id a) `bindM` f = f a
>   runM ~(Id a)      = returnST a


\subsection{Facet monad transformers}
\label{sec:code:action-monad-transformers}

Now we build the monad
transformers representing each facet of action semantics, along with
some extra monad transformers required to make it all happen.  Some of
these are specialisations of the general monad transformers defined
above (Section~\ref{sec:code:general-monad-transformers}).  In building our
final action monad (Section~\ref{sec:code:combined-monad}), we will use these
facet monad transformers.

Note that there is no reflective monad transformer, because the
reflective facet requires no support from the monad!

\subsubsection{List monad transformer}
\label{sec:code:list-monad-transformer}

The list transformer adds nondeterminism to a monad: multiple results
are allowed.

|ListT| (this section) and |NondetT|
(Section~\ref{sec:code:nondeterminism-monad-transformer}) are two alternative
implementations of nondeterminism.  Both turn a |MMonad m| into a
|NondetMMonad m|, with an operator |ambN|.

|ListT| represents nondeterminism by a list of alternatives.  |runM| in
this implementation selects just one of those alternatives.

> data ListT m a = LSM (m [a])

> instance MMonad m => MMonad (ListT m) where

>   unitM v             = LSM (unitM [v])

>   ~(LSM m) `bindM` f
>     = LSM (m                                    `bindM` \vs ->
>            let LSM m' = foldl ambN (LSM (unitM [])) (map f vs)
>            in m')
>     where
>       ambN ~(LSM m1) ~(LSM m2) = LSM (m1        `bindM` \vs1 ->
>                                       m2        `bindM` \vs2 ->
>                                       unitM (vs1 ++ vs2))

Note we duplicate the definition of |ambN| here; otherwise the Gofer
system cannot find it at this point.

>   runM ~(LSM m)       = runM m                  `thenIO` \vs ->
>                         returnST (head vs)

The |head vs| in |runM| is a hack for now; we should choose an element
\emph{randomly} from the list of configurations.

> instance (MMonad m, MMonad (ListT m))
>               => MMonadT ListT m where
>   liftM m             = LSM (m                  `bindM` \v ->
>                              unitM [v])

> class MMonad m => NondetMMonad m where
>   ambN :: m a -> m a -> m a

|ListT| (and also |NondetT|) turn a monad into a |NondetMMonad|, with
one operator.  |m1 `ambN` m2| yields the result of doing either
computation |m1| or computation |m2|.

> instance MMonad m => NondetMMonad (ListT m) where
>   ambN ~(LSM m1) ~(LSM m2) = LSM (m1            `bindM` \vs1 ->
>                                   m2            `bindM` \vs2 ->
>                                   unitM (vs1 ++ vs2))

Notice in the above that monads below (inside) |ListT| will have their
features used multiple times for each possible branch of computation.
Whatever is beneath |ListT| is shared between alternatives.  However,
features above |ListT| are separate.

* instance (NondetMMonad m, MMonadT t m)
*               => NondetMMonad (t m) where
*   ambN m1 m2 = liftM (ambN m1 m2)

|NondetMMonad| has to be lifted separately through each monad
transformer.

> instance (NondetMMonad m, MMonadT (EnvT r') m)
>               => NondetMMonad (EnvT r' m) where
>   ambN ~(EVM m1) ~(EVM m2)
>     = EVM (\r' -> ambN (m1 r') (m2 r'))

> instance (NondetMMonad m, MMonadT (StateT s') m)
>               => NondetMMonad (StateT s' m) where
>   ambN ~(STM m1) ~(STM m2)
>     = STM (\s' -> ambN (m1 s') (m2 s'))

The liftings of |NondetMMonad| through |ListT| and |NondetT| are omitted,
since they would cause
`overlapping instance' errors.  Why?  Because the two monad
transformers would represent exactly the same thing.  This error doesn't
occur when we have two |EnvT|s or two |StateT|s, since they are
parameterised; |ListT| and |NondetT| are not.  Hence we can only have one
level of nondeterminism---not a significant restriction.

> instance (NondetMMonad m, MMonadT ResT m)
>               => NondetMMonad (ResT m) where
>   ambN ~(RSM m1) ~(RSM m2)
>     = RSM (ambN m1 m2)

> instance (NondetMMonad m, MMonadT (ContT ans) m)
>               => NondetMMonad (ContT ans m) where
>   ambN ~(CNM m1) ~(CNM m2)
>     = CNM (\k' -> ambN (m1 k') (m2 k'))

The above apparent duplication of the continuation |k'| may not be
entirely legal (see discussion in Section~\ref{sec:code:parallelism-monad}
relating to the lifting of |ParMMonad| through |ContT|).  It is OK for
|NondetT|, since only one of the two monads will be executed; but for
|ListT| it is incorrect, since both are executed and they must have
different continuations.  In this case, something like the lifting given
for |ParMMonad| through |ContT| should be given, except that this causes
a type error and hence cannot be implemented.


\subsubsection{Nondeterminism monad transformer}
\label{sec:code:nondeterminism-monad-transformer}

The nondeterminism monad transformer is an alternative to the list monad
transformer (Section~\ref{sec:code:list-monad-transformer}).  Instead of
encapsulating a
list of all possibilities, it simply at each stage chooses \emph{one} of the
possibilities.  In all other respects it is the same as the list transformer;
notably, running a |NondetT|-including monad is the same as running a
|ListT|-including monad, assuming that the |runM| randomly selects one option to
pass on from the list.  At least, this is the intention: in the current
implementation, it is not quite true.  See the definition of |ambN|
below.

Note that both |ListT| and |NondetT| turn a |MMonad| into a |NondetMMonad|.  You
shouldn't use both, since they both define an |ambN| operator.

> data NondetT m a = NDM ([Bool] -> m (a,[Bool]))

Note that |NondetT| passes around an infinite list of random booleans:
an infinite random bit stream.  We need a generator for this.  For now,
we use a linear congruential generator,
following~\cite[ch.~3]{Knuth81:Art-Seminumerical}.  The coefficients
in this implementation have not undergone the statistical checks
recommended by Knuth: Caveat user!

We assume a word size of 32 bits, so that 
$m=2^{32}=4,294,967,296$.  We choose $a=314,159,269$, and
$c=1$.  Obviously, we assume silent overflow.

As we should, we treat the (unsigned) result as a binary fraction
between 0 and 1.  However, since the result is actually signed, a
non-negative value corresponds to a binary fraction in $[0,0.5)$ and a
negative value to a binary fraction in $[0.5,1)$.  So we test the sign
of the result, and choose $< 0$ to represent a |1| bit and $\geq 0$ to
represent a |0| bit, with equal probability.

The initial seed is arbitrary.

> randomBitStream :: [Bool]

* randomBitStream = repeat True

> randomBitStream = rbs 6541
>   where rbs :: Int -> [Bool]
>         rbs n = (n<0) : rbs (n*314159269 + 1)

It would perhaps be nice to use the system time as seed here.

\medskip

Back to our scheduled programme\dots

> instance MMonad m => MMonad (NondetT m) where

>   unitM v             = NDM (\n -> unitM (v,n))
>   ~(NDM m) `bindM` f  = NDM (\n -> m n       `bindM` \(v,n') ->
>                                    let NDM m' = f v
>                                    in m' n')
>   runM ~(NDM m)       = runM (m randomBitStream)
>                                              `thenIO` \(v,n) ->
>                         returnST v

> instance (MMonad m, MMonad (NondetT m))
>               => MMonadT NondetT m where
>   liftM m             = NDM (\n -> m         `bindM` \v ->
>                                    unitM (v,n))

The class |NondetMMonad| has already been defined, in
Section~\ref{sec:code:list-monad-transformer}, along with its liftings
through the other monad transformers.

> instance MMonad m => NondetMMonad (NondetT m) where

*   ambN ~(NDM m1) ~(NDM m2)
*     = NDM (\(b:bs) -> m1 bs      `bindM` \(v1,bs1) ->
*                       m2 bs      `bindM` \(v2,bs2) ->
*                       case b of
*                         True  -> unitM (v1,bs1)
*                         False -> unitM (v2,bs2))

I'm not sure my use of |bs| twice is exactly what I want (I guess this
is why a tree of booleans~\cite{Burton88:Nondeterminism} is
preferable).

An alternate definition of |ambN| follows; I'm not sure of its legality.
Whereas the above definition faithfully simulates the behaviour of
|ListT| by doing both monads and then choosing one result, the following
definition cheats by simply choosing one of the \emph{monads} and doing
that only.  Hence the behaviour of levels below |NondetT| is different:
they behave as if they were above, with only the effects of one of the
monads being applied.  This of course speeds up execution immensely, at
some theoretical cost.

>   ambN ~(NDM m1) ~(NDM m2)
>     = NDM (\(b:bs) -> case b of
>                         True  -> m1 bs
>                         False -> m2 bs)


\subsubsection{Resumption monad transformer}
\label{sec:code:resumption-monad-transformer}

The resumption monad transformer changes the monad into one that
features resumptions: interruptible computations.

This is represented by instantiating the monad over
\emph{configurations:} a computation is either \emph{complete}, giving a
final result, or \emph{incomplete}, with an intermediate state
representing the remainder of the computation.

\smallskip

Most of the trickery here and in |ListT|
(Section~\ref{sec:code:list-monad-transformer}) ultimately derives from
\cite{Espinosa95:Semantic}, especially pp.~32--37, 108, 110 and~124.

> data ResT m a = RSM (m (Cfg m a))
> data Cfg m a = Final a | Inter (ResT m a)

> instance MMonad m => MMonad (ResT m) where

>   unitM v
>     = RSM (unitM (Final v))

>   ~(RSM m) `bindM` f
>     = RSM (m                                   `bindM` \c ->
>            case c of
>              Final v0 -> let RSM m' = f v0
>                          in m'
>              Inter r0 -> unitM (Inter (r0 `bindM` f)))

>   runM ~(RSM f)
>     = runM (final f) `thenIO` \v ->
>       returnST v
>     where
>    -- final :: m (Cfg m a) -> m a
>       final f = f                              `bindM` \c ->
>                 case c of
>                   Final v       -> unitM v
>                   Inter (RSM r) -> final r

Note that anything \emph{outside} the resumption transformer will be
paused and resumed as expected, but anything \emph{inside} the
resumption transformer will \emph{not} be paused and resumed, but be
used sequentially during execution of all parallel threads.  In other
words, anything inside |ResT| will interfere between threads, whereas
anything outside it will be separate.  This means that you will probably
want to place stores inside |ResT|, but environments outside it.

> instance (MMonad m, MMonad (ResT m))
>               => MMonadT ResT m where
>   liftM m             = RSM (m                 `bindM` \v ->
>                              unitM (Final v))

> class MMonad m => ResMMonad m where
>   pauseR :: m a -> m a
>   indivR :: m a -> m a

|ResT| converts a monad into a |ResMMonad|, offering two operators.
|pauseR m| pauses a computation, adding a point at which it can be
interrupted.  |indivR m| removes all interruptible points from a
computation, and makes it execute in a single step (\emph{indivisibly}).

> instance MMonad m => ResMMonad (ResT m) where
>   pauseR ~(RSM r)
>     = RSM (r                                   `bindM` \c ->
>            unitM (Inter (RSM (unitM c))))
>   indivR ~(RSM r)
>     = RSM (indivR' r)
>     where indivR' r = r                        `bindM` \c ->
>                      case c of
>                        Final v        -> unitM (Final v)
>                        Inter (RSM r') -> indivR' r'

* instance (ResMMonad m, MMonadT t m) => ResMMonad (t m) where
*   pauseR m1         = liftM (pauseR m1)
*   indivR m1         = liftM (indivR m1)

|ResMMonad| must be lifted through each monad transformer separately.

> instance (ResMMonad m, MMonadT (EnvT r') m)
>               => ResMMonad (EnvT r' m) where
>   pauseR ~(EVM m1)  = EVM (\r' -> pauseR (m1 r'))
>   indivR ~(EVM m1)  = EVM (\r' -> indivR (m1 r'))

> instance (ResMMonad m, MMonadT (StateT s') m)
>               => ResMMonad (StateT s' m) where
>   pauseR ~(STM m1)  = STM (\s' -> pauseR (m1 s'))
>   indivR ~(STM m1)  = STM (\s' -> indivR (m1 s'))

> instance (ResMMonad m, MMonadT ListT m)
>               => ResMMonad (ListT m) where
>   pauseR ~(LSM m1)  = LSM (pauseR m1)
>   indivR ~(LSM m1)  = LSM (indivR m1)

> instance (ResMMonad m, MMonadT NondetT m)
>               => ResMMonad (NondetT m) where
>   pauseR ~(NDM m1)  = NDM (\n' -> pauseR (m1 n'))
>   indivR ~(NDM m1)  = NDM (\n' -> indivR (m1 n'))

The lifting of |ResMMonad| through |ResT| is omitted, as it is not
required and we would get an ``overlapping instance'' type error.

> instance (ResMMonad m, MMonadT (ContT ans) m)
>               => ResMMonad (ContT ans m) where
>   pauseR ~(CNM m1)  = CNM (\k' -> pauseR (m1 k'))
>   indivR ~(CNM m1)  = CNM (\k' -> indivR (m1 k'))


\subsubsection{Parallelism monad}
\label{sec:code:parallelism-monad}

Once we have a |ResMMonad| that is also a |NondetMMonad|, we have the
features required for a |ParMMonad|---parallelism.  Note that this
|ParMMonad| does not have a separate monad transformer of its own---it
automatically follows from any monad with both resumptions and
nondeterminism.  Recommended transformers to use are |ResT|
(Section~\ref{sec:code:resumption-monad-transformer}) and |NondetT|
(Section~\ref{sec:code:nondeterminism-monad-transformer}).

\medskip

The parallelism monad enables parallelism, by combining nondeterminism
from |NondetMMonad| and resumptions from |ResMMonad|.  Resumptions allow
us to execute different threads in a ``time-sliced'' manner, and
nondeterminism allows us to schedule the time slices in a
non-determinate manner.

> class (ResMMonad m, NondetMMonad m) => ParMMonad m where
>   par'P  :: m a -> m a -> (Int -> m a -> m a -> m b) -> m b
>   parP   :: m a -> m a -> m a

The |ParMMonad| features two operators.  |par'P m1 m2 com| executes the
two monads given in parallel (preserving in all recursive calls the
order of the arguments).  When one monad completes, |com| is called (as
|com n m1' m2'|), with an integer |1| or |2| to indicate which monad
completed, a monad encapsulating the final state of the completed monad,
and the remainder of the other monad.

|parP m1 m2| is a simple specialisation of |par'P|; it runs both monads in
parallel and returns the result of the last one to complete, throwing
the other result away.

> instance NondetMMonad m => ParMMonad (ResT m) where

>   par'P ~(RSM r1) ~(RSM r2) combine
>     = RSM ((then' 1 r1 r2) `ambN` (then' 2 r2 r1))
>     where
>       then' n r1 r2
>         = r1                `bindM` \c ->
>           case c of
>             Final v1
>              -> let RSM r'
>                   = pauseR (combine n (unitM v1) (RSM r2))
>                 in r'
>             Inter r1'
>              -> let RSM r'
>                   = pauseR (case n of
>                              1 -> par'P r1' (RSM r2) combine
>                              2 -> par'P (RSM r2) r1' combine)
>                 in r'

>   parP r1 r2
>     = par'P r1 r2 (\n r1 r2 -> case n of
>                                  1 -> r2
>                                  2 -> r1)

* instance (ParMMonad m, MMonadT t m) => ParMMonad (t m) where
*   par'P m1 m2 com = liftM (par'P m1 m2 com)
*   parP  m1 m2     = liftM (parP  m1 m2)

Of course the above liftings don't work; we need to lift |ParMMonad|
separately through each transformer.

\smallskip

In the code below, note something interesting: every feature added on
top of the |ParMMonad| will behave in a rather strange manner with
regard to |com|.  In |com n m1 m2|, the monads |m1| and |m2|
will ignore the values of features above the |ParMMonad| passed to them,
and use their own internal values.  The values of those features when
passed to |combine| are indeterminate---what values should be passed?
Those of the computation of |m1| or those of |m2|?  Since there is no
right answer here, we merely pass in $\perp$, causing an error if an
attempt is made to look at the values.  See log: 1996-11-20.

> instance (ParMMonad m, MMonadT (EnvT r') m)
>               => ParMMonad (EnvT r' m) where
>   par'P ~(EVM m1) ~(EVM m2) com
>     = EVM (\r' ->
>         let com' n m1' m2'
>          = let EVM m' = com n (EVM (\_ -> m1'))
>                               (EVM (\_ -> m2'))
>            in (m' (error "EnvT value undefined in com'"))
>         in par'P (m1 r') (m2 r') com')
>   parP  ~(EVM m1) ~(EVM m2) = EVM (\r' -> parP (m1 r') (m2 r'))

> instance (ParMMonad m, MMonadT (StateT s') m)
>               => ParMMonad (StateT s' m) where
>   par'P ~(STM m1) ~(STM m2) com
>     = STM (\s' ->
>         let com' n m1' m2'
>          = let STM m' = com n (STM (\_ -> m1'))
>                               (STM (\_ -> m2'))
>            in (m' (error "StateT value undefined in com'"))
>         in par'P (m1 s') (m2 s') com')
>   parP  ~(STM m1) ~(STM m2) = STM (\s' -> parP (m1 s') (m2 s'))

Note that we copy (i.e., duplicate) the state here.  Any |StateT|
outside |ParMMonad| will \emph{not} interfere between threads.

\medskip

The liftings of |ParMMonad| through |ListT|, |NondetT| and |ResT| are
omitted, as they are not required: neither can be above |ParMMonad|
anyway.

\medskip

The lifting of |ParMMonad| through |ContT| is commented out.  It causes
a type error: `declared type too general'.  |ContT| won't let |par'P|'s
result type be different from the types of its arguments.

We can't simply follow the pattern established above.  This
would involve passing |k'| to both |m1| and |m2| in the call to the
next-level |par'P|---in other words, telling both |m1| and |m2| that
their continuation is that of the |par'P| as a whole.  Both of these
would be lies: their continuations are to have their values combined by
|com'| and then passed to |k'|.

\smallskip

We could achieve the lifting using the following definition:

* instance (ParMMonad m, MMonadT (ContT ans) m)
*               => ParMMonad (ContT ans m) where
*   par'P ~(CNM m1) ~(CNM m2) com
*     = CNM (\k' -> let com' n m1' m2'
*                         = let CNM m' = com n (CNM (\_ -> m1'))
*                                              (CNM (\_ -> m2'))
*                           in (m' k')
*                   in par'P (m1 unitM) (m2 unitM) com')

This works by passing an identity continuation to |m1| and |m2| (acting
similarly to \emph{prompt}~\cite{Sabry*93:Reasoning-Continuations}),
taking the results from each, combining them, and then producing the
result.

However, this still restricts the type too much: the type of
|par'P| becomes 
\[\texttt{m ans -> m ans -> (Int -> m ans -> m ans -> m b) -> m b}\]
i.e.,
the two component monads must be over type |ans| rather than over some
unspecified type |a|.  This is unacceptable.


\subsubsection{Basic and functional monad transformer}
\label{sec:code:bf-monad-transformer}

The basic and functional monad transformer is actually two transformers.
We have |UnfoldT|, which adds an environment holding the action to replace
|aUnfold| by, and |BehavT|, which adds |State| (i.e.,
|(Behaviour,| |Commitment)|) as state.  These two are required to
support the first two facets of action semantics.

> type BasFunT m = UnfoldT (BehavT m)

We split |BasFunT| into its two logical components here, to allow the
automatic lifting machinery to work properly.

> type BehavT = StateT State
> type UnfoldT = EnvT Abstraction

Gofer won't let us do |EnvT Action| here because it would be a
recursive type synonym.

\smallskip

Unfortunately, we must duplicate the definitions for |unitM| and |bindM|
here, since |runM| is different and Gofer class instances are
all-or-nothing.

> instance MMonad m => MMonad (BehavT m) where

>   unitM v             = STM (\b -> unitM (v,b))
>   ~(STM m) `bindM` f  = STM (\b -> m b       `bindM` \(v,b') ->
>                                    let STM m2 = f v
>                                    in m2 b')
>   runM ~(STM f) = runM (f (State (Tr tnil) Unc))
>                                              `thenIO` \(v,b) ->
>                   returnST v

> instance MMonad m => MMonad (UnfoldT m) where
>   unitM v             = EVM (\_ -> unitM v)
>   ~(EVM m) `bindM` f  = EVM (\r -> m r       `bindM` \v ->
>                                    let EVM m2 = f v
>                                    in m2 r)
>   runM ~(EVM f) = runM (f (abstractAct nop)) `thenIO` \v ->
>                   returnST v

> class MMonad m => BehavMMonad m where
>   getB  ::  m Behaviour
>   doB   ::  Behaviour -> m ()
>   getX  ::  m Commitment
>   setX  ::  Commitment -> m ()
>   unX   ::  m ()
>   orX   ::  Commitment -> m ()

|BehavT| turns a monad into a |BehavMMonad|, with six operators.  |getB|
and |doB| respectively get and set the |Behaviour|; |getX| and |setX| do
the same for the |Commitment|.  |unX| clears the commitment, and |orX|
|orCom|s a commitment onto the existing commitment.

> class MMonad m => UnfoldMMonad m where
>   withA ::  Action -> m a -> m a
>   rdA   ::  m Action

|UnfoldT| turns a monad into an |UnfoldMMonad|, with two operators.
The operator |withA a m| performs |m| in an environment containing
|a| as the stored action; |rdA| reads the current action.

> instance (MMonad m, StateMMonad State (BehavT m))
>               => BehavMMonad (BehavT m) where
>   getB    = getState                    `bindM` \(State b _) ->
>             unitM b
>   doB b   = getState                    `bindM` \(State _ x) ->
>             setState (State b x)
>   getX    = getState                    `bindM` \(State _ x) ->
>             unitM x
>   setX x1 = getState                    `bindM` \(State b _) ->
>             setState (State b x1)
>   unX     = getState                    `bindM` \(State b _) ->
>             setState (State b Unc)
>   orX x1  = getState                    `bindM` \(State b x) ->
>             setState (State b (x `orCom` x1))

> instance (MMonad m, EnvMMonad Abstraction (UnfoldT m))
>               => UnfoldMMonad (UnfoldT m) where
>   withA a = inEnv (abstractAct a)
>   rdA     = rdEnv `bindM` \aa -> unitM (enactAbs aa)

> instance (BehavMMonad m, MMonadT t m)
>               => BehavMMonad (t m) where
>   getB    = liftM getB
>   doB b   = liftM (doB b)
>   getX    = liftM getX
>   setX c1 = liftM (setX c1)
>   unX     = liftM unX
>   orX c1  = liftM (orX c1)

> instance (UnfoldMMonad m, MMonadT t m)
>               => UnfoldMMonad (t m) where
>   rdA     = liftM rdA
>-- withA a = liftM (withA a)

Unfortunately, as the |--| signifies, the above |withA| definition
doesn't work.  Hence we must lift it separately through
each monad transformer.

> instance (UnfoldMMonad m, MMonadT (StateT s') m)
>               => UnfoldMMonad ((StateT s') m) where
>   rdA     = liftM rdA
>   withA a ~(STM m) = STM (\s' -> withA a (m s'))

> instance (UnfoldMMonad m, MMonadT (EnvT r') m)
>               => UnfoldMMonad ((EnvT r') m) where
>   rdA     = liftM rdA
>   withA a ~(EVM m) = EVM (\r' -> withA a (m r'))

> instance (UnfoldMMonad m, MMonadT ListT m)
>               => UnfoldMMonad (ListT m) where
>   rdA     = liftM rdA
>   withA a ~(LSM m) = LSM (withA a m)

> instance (UnfoldMMonad m, MMonadT NondetT m)
>               => UnfoldMMonad (NondetT m) where
>   rdA     = liftM rdA
>   withA a ~(NDM m) = NDM (\n' -> withA a (m n'))

> instance (UnfoldMMonad m, MMonadT ResT m)
>               => UnfoldMMonad (ResT m) where
>   rdA     = liftM rdA
>   withA a ~(RSM m) = RSM (withA a m)

> instance (UnfoldMMonad m, MMonadT (ContT ans) m)
>               => UnfoldMMonad ((ContT ans) m) where
>   rdA     = liftM rdA
>   withA a ~(CNM m) = CNM (\k' -> withA a (m k'))


\subsubsection{Declarative monad transformer}
\label{sec:code:declarative-monad-transformer}

The declarative monad transformer adds |Environment| (as a state) to the
monad.

> type DecT = StateT Environment

> instance MMonad m => MMonad (DecT m) where
>   unitM v             = STM (\e -> unitM (v,e))
>   ~(STM m) `bindM` f  = STM (\e -> m e       `bindM` \(v,e') ->
>                                    let STM m2 = f v
>                                    in m2 e')
>   runM ~(STM f) = runM (f emptyEnv)          `thenIO` \(v,e) ->
>                   returnST v

> class MMonad m => DecMMonad m where
>   getE :: m Environment
>   setE :: Environment -> m ()

|DecT| transforms a monad into a |DecMMonad|, offering two operators.
|getE| examines the current environment, and |setE e| updates it.

\medskip

> instance (MMonad m, StateMMonad Environment (DecT m))
>               => DecMMonad (DecT m) where
>   getE   = getState
>   setE   = setState

Lifting |DecMMonad| is straightforward.

> instance (DecMMonad m, MMonadT t m) => DecMMonad (t m) where
>   getE   = liftM getE
>   setE e = liftM (setE e)


\subsubsection{Imperative monad transformer}
\label{sec:code:imperative-monad-transformer}

The imperative monad transformer adds a |Store| (as state) to the monad.

> type ImpT = StateT Store

> instance MMonad m => MMonad (ImpT m) where
>   unitM v             = STM (\s -> unitM (v,s))
>   ~(STM m) `bindM` f  = STM (\s -> m s       `bindM` \(v,s') ->
>                                    let STM m2 = f v
>                                    in m2 s')
>   runM ~(STM f) = runM (f emptyStore)        `thenIO` \(v,s) ->
>                   returnST v

> class MMonad m => ImpMMonad m where
>   getS :: m Store
>   setS :: Store -> m ()

|ImpT| turns a monad into an |ImpMMonad|, with two operators.  |getS|
examines the store, and |setS s| updates it.

> instance (MMonad m, StateMMonad Store (ImpT m))
>               => ImpMMonad (ImpT m) where
>   getS   = getState
>   setS   = setState

Lifting |ImpMMonad| is straightforward.

> instance (ImpMMonad m, MMonadT t m) => ImpMMonad (t m) where
>   getS   = liftM getS
>   setS s = liftM (setS s)


\subsubsection{Communicative monad transformer}
\label{sec:code:communicative-monad-transformer}

The communicative monad transformer adds (as state) a |Communication| to
the monad.  This |Communication| (see Section~\ref{sec:code:communications})
stores an input buffer and a copy of the |RealWorld|, used for doing
input and output.

> type CommT = StateT Communication

> instance MMonad m => MMonad (CommT m) where
>   unitM v             = STM (\c -> unitM (v,c))
>   ~(STM m) `bindM` f  = STM (\c -> m c       `bindM` \(v,c') ->
>                                    let STM m2 = f v
>                                    in m2 c')
>   runM ~(STM f) = getworldST            `thenIO` \w ->
>                   runM (f (w,Nothing))  `thenIO` \(v,(w',_)) ->
>                   setworldST w'         `thenIO` \() ->
>                   returnST v

Note the way we use the new operators |getworldST| and |setworldST| to
get access to the internal |RealWorld| value, passing it through the
monad to drive the I/O (see Section~\ref{sec:code:communications}).

> class MMonad m => CommMMonad m where
>   sendC    :: Transient -> m ()
>   wipebufC :: m ()
>   getbufC  :: m (Maybe Transient)

|CommT| turns a monad into a |CommMMonad|, with three operators. 
|sendC t| outputs a transient on standard output.  |wipebufC| clears
the input buffer.  And |getbufC| obtains the current value stored in the
input buffer, if any.  Note that currently, |getbufC| \emph{blocks} if
the input buffer is empty, waiting for input before continuing.  This
causes some problems for parallelism.

> instance (MMonad m, StateMMonad Communication (CommT m))
>               => CommMMonad (CommT m) where

>   sendC t  = getState                       `bindM` \(w,buf) ->
>              let (v,w') = semisafeRunST (putTransient t) w
>              in setState ((w',buf)::Communication)
>                                             `bindM` \() ->
>                 unitM v

>   wipebufC = getState                       `bindM` \(w,buf) ->
>              let z = (w,buf)::Communication
>              in setState ((w,Nothing)::Communication)

>   getbufC  = getState                       `bindM` \(w,buf) ->
>              case buf of
>                Just _
>                 -> unitM buf
>                Nothing
>                 -> let (v,w') = semisafeRunST getTransient w
>                    in setState (w',Just v)  `bindM` \() ->
>                       unitM (Just v)

Note here how we use the |RealWorld| value to sequence all our I/O
operations, by passing it through |semisafeRunST|.

Annoyingly, the type inference system is unable to get enough
information from the above definitions without some explicit typing;
hence the explicit types given above.  The problem is that Gofer uses
the type of the argument to |setState|/|getState| to determine which
monad transformer to access for the answer; and |buf| is unconstrained
by |sendC|'s and |wipebufC|'s definitions.

\medskip

Lifting |CommMMonad| is straightforward.

> instance (CommMMonad m, MMonadT t m) => CommMMonad (t m) where
>   sendC t  = liftM (sendC t)
>   wipebufC = liftM wipebufC
>   getbufC  = liftM getbufC


\subsubsection{Directive monad transformer}
\label{sec:code:directive-monad-transformer}

The directive monad transformer adds (as state) a |Redirection| to the
monad.  This supports directive-facet operations.

> type DirT = StateT Redirection

> instance MMonad m => MMonad (DirT m) where
>   unitM v             = STM (\d -> unitM (v,d))
>   ~(STM m) `bindM` f  = STM (\d -> m d       `bindM` \(v,d') ->
>                                    let STM m2 = f v
>                                    in m2 d')
>   runM ~(STM f) = runM (f emptyRedirection)  `thenIO` \(v,d) ->
>                   returnST v

> class MMonad m => DirMMonad m where
>   getD :: m Redirection
>   setD :: Redirection -> m ()

|DirT| turns a monad into a |DirMMonad|, with two operators.  |getD|
access the current redirection, and |setD d| sets it.

> instance (MMonad m, StateMMonad Redirection (DirT m))
>               => DirMMonad (DirT m) where
>   getD   = getState
>   setD   = setState


Lifting |DirMMonad| is straightforward.

> instance (DirMMonad m, MMonadT t m) => DirMMonad (t m) where
>   getD   = liftM getD
>   setD d = liftM (setD d)


\subsubsection{Continuation monad transformer}
\label{sec:code:continuation-monad-transformer}

The continuation monad transformer is for an experimental new facet for
action semantics.  It changes a monad to use the continuation-passing
style.

This is achieved by turning the monad into a function from a
continuation to a computation over some answer type.  A continuation is
simply a function from the value type to a computation over the answer
type.

> data ContT ans m a = CNM ((a -> m ans) -> m ans)

Note that ideally, |ContT| would be polymorphic in |ans|; however this
is untypable in Gofer, and so we must specify it.  This static fixing of
the answer type causes a number of problems throughout the code; however
we manage to make (most) things work.

The |ans|wer type here will depend on the monad transformers above this
one in the stack of transformers.  Assuming the monad is finally to be
|runM|'d, it will be |()| if |ContT| is at the top, |((),S)| if it is
surrounded by |StateT S|, |(((),R),S)| if it is surrounded by
|EnvT R .| |StateT S|, etc.

Also dependent on where |ContT| appears in the stack of monad
transformers is the subset of features which are saved by |callccK|:
every transformer \emph{outside} |ContT| has its state preserved by
|callccK| and restored when the continuation is invoked; transformers
\emph{inside} |ContT| have their current state passed dynamically
(\emph{this includes environment transformers!}).

Note that unfortunately the state of the world cannot be saved and
restored, and so |CommT| (see
Section~\ref{sec:code:communicative-monad-transformer}) should always appear
\emph{inside} |ContT|;
if it appears outside, it will behave (anomalously) as if it is inside,
in the process violating the constraints on the use of the |RealWorld|
value obtained by |getworldST|.

> instance MMonad m => MMonad (ContT ans m) where
>   unitM v             = CNM (\k -> k v)
>   ~(CNM m) `bindM` f  = CNM (\k -> m (\a -> let CNM f' = f a
>                                             in f' k))
> --runM ~(CNM f)       = runM (f unitM) `thenIO` \ans ->
> --                      returnST ans

|runM| as defined above will not get past the type system, unfortunately, 
because it constrains the |a| of |runM|'s type (|m a| |-> IO a)| and the
|ans| of |ContT| to be the same type
(|f :: (a| |-> m ans)| |-> m ans|, hence
|unitM :: a| |-> m ans|, but |unitM :: a| |-> m a|, hence
|a|~$\equiv$~|ans|),
conflicting with the fact that |a| is free and |ans| is
fixed at the time of the definition of the monad
(Section~\ref{sec:code:combined-monad}).  This can be worked around by simply
defining (a function identical to) |runM| \emph{outside} the monad: we
do this in Section~\ref{sec:code:combined-monad} with |runM'|.

> instance (MMonad m, MMonad (ContT ans m))
>               => MMonadT (ContT ans) m where
>   liftM m             = CNM (\k -> m `bindM` k)

> class MMonad m => ContMMonad m where
>   callccK :: ((a -> m b) -> m a) -> m a

|ContT| turns a monad into a |ContMMonad|, with one operator. 
|callccK f| calls the function |f|, passing it the current continuation
as argument.

> instance MMonad m => ContMMonad (ContT ans m) where
>   callccK f
>    = CNM (\k -> let CNM f' = f (\a -> CNM (\_ -> k a))
>                 in f' k)

|ContMMonad|s must be lifted separately through each transformer:

> instance (ContMMonad m, MMonadT (EnvT r') m)
>               => ContMMonad (EnvT r' m) where
>   callccK f
>    = EVM (\r -> callccK (\k ->
>                   let EVM f' = f (\a -> EVM (\_ -> k a))
>                   in f' r))

> instance (ContMMonad m, MMonadT (StateT s') m)
>               => ContMMonad (StateT s' m) where
>   callccK f
>    = STM (\s0 -> callccK (\k ->
>                    let STM f' = f (\a -> STM (\_ -> k (a,s0)))
>                    in f' s0))

We here use the `debugging' |callccK| semantics for stores, rather than the
`usual' semantics (see \cite[sec.~8.3]{Liang*95:Monad} for further
explanation).  In other words, if |StateT| appears \emph{outside}
|ContT|, then it will be saved by |callccK| and restored when the
captured continuation is invoked; the `usual' semantics neither saves
nor restores the state.

We do this to be able to obtain different behaviour
from the combined monad depending on whether the state transformer in
question appears inside or outside |ContT| (see
Section~\ref{sec:code:environment-monad-transformer}).  To get the `usual'
semantics, simply change |STM (\_ ->| |k (a,s0))| above to
|STM (\s1 ->| |k (a,s1))|.

> instance (ContMMonad m, MMonadT ListT m)
>               => ContMMonad (ListT m) where
>   callccK f
>     = LSM (callccK (\k ->
>              let LSM f' = f (\a -> LSM (k [a]     `bindM` \v ->
>                                         unitM [v]))
>              in f'))

> instance (ContMMonad m, MMonadT NondetT m)
>               => ContMMonad (NondetT m) where
>   callccK f
>    = NDM (\n0 -> callccK (\k ->
>                    let NDM f' = f (\a -> NDM (\n1 -> k (a,n0)))
>                    in f' n0))

Again, note that the above is the `debugging' semantics (see lifting
through |StateT|) for nondeterminism.

> instance (ContMMonad m, MMonadT ResT m)
>               => ContMMonad (ResT m) where
>   callccK f
>     = RSM (callccK (\k ->
>              let RSM f'
>               = f (\a -> RSM (k (Final a)         `bindM` \v ->
>                          unitM (Final v)))
>              in f'))

We don't lift |ContMMonad| through |ContT|, since the answer type must
be unique and hence both |ContMMonad|s would be parameterised by the
same type, thereby causing an `overlapping instance' error.


\subsection{The combined monad}
\label{sec:code:combined-monad}

The combined monad is built from the transformers desired from the
selection above, on top of the |Id| base monad.

\medskip

The following is the recommended monad type to use to include all the
features.  Why?  Let's see:
\begin{itemize}
\item |BasFunT|, at the top, represents the basic and functional facets.
This means it handles completion, escapes and failure, and the data
associated with completion and escapes.  It also handles unfolding.
\item |DecT|, next, represents the declarative facet, and handles
environments.  This, along with |BasFunT|, must be above |ResT| (if
included) to get the expected behaviour for the action combinators.
\item |ResT| handles resumptions, allowing computations to be
interrupted and resumed, hence enabling parallel execution (for constructs
like |cAnd|).  All features above |ResT| are \emph{non-interfering} between
threads: each thread has its own copy.  Features below |ResT|, however,
may interfere---there is only one shared copy of them all, shared
between all threads.
\item |ContT| represents the continuational facet.  It handles
continuations.  Like |ResT|, everything above it is non-interfering and
restored when a continuation is invoked; everything below it is shared.
The type passed it as an argument, the `answer' type, is the monad
argument type at this level, assuming the whole monad is instantiated
over the type |()|.

Note that |ResT| has to be placed above |ContT|, as it cannot be lifted
through it for reasons discussed in Section~\ref{sec:code:parallelism-monad}.
\item |ImpT| represents the imperative facet, i.e., stores.
\item |DirT| represents the directive facet, i.e., redirections.
\item |NondetT| handles nondeterminism.  |ListT| could work equally well
here; however |NondetT| is more efficient for our purposes, evaluating
only one execution path.  This is a requirement, along with |ResT|, to
provide parallelism.

Anything above |NondetT| (or |ListT|) is subject to nondeterminism
(i.e., multiple possibilities); however, anything \emph{below} this
transformer is shared between all possibilities.  Ideally this would be
nothing; however since we can't have multiple instances of the real
world floating around, |CommT|, encapsulating a |RealWorld| value, must
sit beneath |NondetT| and take the consequences.
\item |CommT| represents the communicative facet.  It handles
communication with the outside world, by encapsulating an object of type
|RealWorld|.
\end{itemize}

> type M = (BasFunT
>          (DecT
>          (ResT
>          (ContT (((),State),Environment)
>          (ImpT
>          (DirT
>          (NondetT        -- or ListT
>          (CommT
>             Id))))))))

The following definition contains just Mosses' action semantics, with
no extensions.

* type M = (BasFunT
*          (DecT
*          (ResT
*          (ImpT
*          (DirT
*          (NondetT
*          (CommT
*             Id)))))))

The following definition is for the sequential version of this action
semantics (see Section~\ref{sec:code:handling-omissions}).

* type M = (BasFunT
*          (DecT
*          (ImpT
*          (DirT
*          (CommT
*             Id)))))


\subsubsection{Top-level \texttt{runM'}}
\label{sec:code:top-level-runM'}

Now we define |runM'|, which is the same as |runM| restricted to actions
only (i.e., monads over |()|), but lives outside the
monad.  This is for the benefit of |ContT|, whose |runM| breaks the type
system (see Section~\ref{sec:code:continuation-monad-transformer}).

Its definition depends on the location of |ContT| in the stack
of transformers defining |M|; however the definition consists merely of
a combination of the |runM| definitions found for each transformer---the
code is identical, only the type is different (it is more specific and
no longer polymorphic).

> runM' :: Action -> IO ()

The following definition is for the first, preferred definition of |M|.

> runM' act = runM'1 act 
>   where
>     runM'1 ~(EVM f) = runM'2 (f (abstractAct nop))
>                                              `thenIO` \v ->
>                       returnST v
>     runM'2 ~(STM f) = runM'3 (f (State (Tr tnil) Unc))
>                                              `thenIO` \(v,_) ->
>                       returnST v
>     runM'3 ~(STM f) = runM'4 (f emptyEnv)    `thenIO` \(v,_) ->
>                       returnST v
>     runM'4 ~(RSM f) = runM'5 (final f)       `thenIO` \v ->
>                       returnST v
>  -- final :: m (Cfg m a) -> m a
>     final f = f                              `bindM` \c ->
>               case c of
>                 Final v       -> unitM v
>                 Inter (RSM r) -> final r
>     runM'5 ~(CNM f) = runM (f unitM)         `thenIO` \ans ->
>                       returnST ans

This assumes |ContT| is surrounded by |ResT|, |DecT| and
then |BasFunT|, in that order.

\medskip

The following definition will serve for any definition of |M| not
including |ContT|:

* runM' act = runM act


\subsubsection{Handling omissions from the combined monad}
\label{sec:code:handling-omissions}

The idea of monad transformers is that the transformers can be combined
in different ways to yield different monads with equivalent external
behaviour except for the features explicitly included or excluded.

This modular monadic action semantics system depends in various places
on various features of the combined monad.  These are documented in this
section.

\begin{enumerate}

\item Pretty much everything depends on $EBX$ being there (i.e.,
|BasFunT| and |DecT|).  Mosses' whole concept of how the combinators
work, for example, makes no sense without these three levels.

\item The combinators (and certain actions) have been written to use
parallelism where they are supposed to (according
to~\cite{Mosses92:Action}); if |ResT| and |NondetT| (or |ListT|) are not
included, then this is not possible: |par'P|, |pauseR|, |indivR| and |ambN|
all disappear.  The code can still work in this case, with a few changes
to make it purely sequential---in fact, this program was entirely
sequential for many months until parallelism was later added.

Doing the following will cause the semantics to become sequential and
deterministic:
\begin{itemize}
\item Replace the definition of |bincompar| in
  Section~\ref{sec:code:combinators} with the |*|'d out version.
\item In the first line of the definition of |cOr| in
  Section~\ref{sec:code:combinators-basic-and-functional}, comment out the
  text from |`ambN`| to the end of the line (with |{-|$\cdots$|-}|).
\item In the definition of |cIndivisibly| in the same section, comment
  out the occurrence of |indivR|.
\item In the definition of |aChoose| in
  Section~\ref{sec:code:actions-basic-and-functional}, in the third case of
  |aChoose'|, comment out from |`ambN`| to the end of the line.
\item Comment out the occurrences of |pauseR| in |aUnfold|
  and |aDiverge| (Section~\ref{sec:code:actions-basic-and-functional}),
  in |bincom| (Section~\ref{sec:code:combinators-basic-and-functional}), and
  in |aEnact| (Section~\ref{sec:code:actions-reflective}).
\item Comment out occurrences of |indivR| in the combinator
  |cPatiently| (Section~\ref{sec:code:combinators-communicative}) and
  in |aRecursivelyBindTo| (Section~\ref{sec:code:actions-directive}).
\end{itemize}

\item |runMD| (Section~\ref{sec:code:debugging}) can be edited to remove
references to features that have been removed (just delete the
appropriate |get*| and |shows| lines); however it will not work without
a means of writing its output: |CommT|.

\item Obviously, the `*' facet requires the `*' transformer to be present in
most cases.  To avoid errors, simply comment out the appropriate action,
combinator and yielder sections with `|> {-|' and `|> -}|' lines.

\end{enumerate}


\subsubsection{Debugging}
\label{sec:code:debugging}

To debug actions, it is useful to know the final state after an action
has run.  |runMD| runs an action and then displays the final state; it
uses |CommT| to do the display, so it must be included in the monad.

> runMD :: Action -> IO ()

> runMD act = runM' (act  `bindM` \() ->
>                    getB `bindM` \b ->
>                    getX `bindM` \c ->
>                    getE `bindM` \e ->
>                    getS `bindM` \s ->
>                    getD `bindM` \d ->
>                    sendC (inj (nl . shows b . showChar ' '
>                                   . shows c . nl
>                                   . shows e . nl
>                                   . shows s . nl
>                                   . shows d
>                                   $ "")))
>   where nl = showChar '\n'


\subsection{Instantiations}
\label{sec:code:instantiations}

There are two key instantiations of our action monad type |M|:
|Action| and |Yielder|.

An \emph{action} is represented by an action monad over
the unit type, since an action has no return value.

> type Action = M ()

A \emph{yielder} is represented by an action monad over the data type
|Transient|, representing the return value of the yielder.

> type Yielder = M Transient

Note that there is in reality an additional restriction on yielders:
they must only \emph{read} the state: they are not allowed to modify it
in any way.  This is at present unenforced, unfortunately.


\section{Action Notation}
\label{sec:code:action-notation}

This section contains a definition of action notation using the action
monad defined above.  The semantics of each action, combinator, yielder
and data operation follows that of Mosses' Action Notation, as specified
in Appendices~B--E of~\cite{Mosses92:Action}, except where
noted.


\subsection{Actions}
\label{sec:code:actions}

Firstly, we define the \emph{actions} of action semantics.  We do this
by facet, except that there is no separate hybrid facet (instead
|aAllocate| is defined with the imperative actions, and |aReceive| and
|aSubordinate| are omitted), and the basic and functional actions are
defined together.


\subsubsection{Basic and Functional}
\label{sec:code:actions-basic-and-functional}

We now build the basic and functional facets' actions on top of
the monad.

\medskip

A useful support function is |wipeenv|, which wipes all bindings.  All
basic and functional actions do this.

> wipeenv :: Action
> wipeenv = setE emptyEnv

> aComplete, aEscape, aFail, aDiverge, aCommit :: Action
> aEscapeWith :: Yielder -> Action
> aGive       :: Yielder -> Action
> aRegive     :: Action
> aChoose     :: Yielder -> Action
> aCheck      :: Yielder -> Action
> aUnfold     :: Action

These actions are all per Mosses except for |aChoose|, which chooses an
element nondeterministically from a tuple rather than from a sort.

> aComplete      = wipeenv                         `bindM` \() ->
>                  doB (Tr tnil)

> aEscape        = yIt                             `bindM` \t ->
>                  wipeenv                         `bindM` \() ->
>                  doB (Esc t)

> aFail          = wipeenv                         `bindM` \() ->
>                  doB Fail

> aDiverge       = pauseR aDiverge

> aCommit        = orX Com                         `bindM` \() ->
>                  aComplete

> aEscapeWith yt = yt                              `bindM` \t ->
>                  wipeenv                         `bindM` \() ->
>                  doB (Esc t)

> aGive yt       = yt                              `bindM` \t ->
>                  wipeenv                         `bindM` \() ->
>                  doB (Tr t)

> aRegive        = wipeenv

> aChoose yts    = yts                             `bindM` \t ->
>                  wipeenv                         `bindM` \() ->
>                  aChoose' (prj1' t "aChoose")
>   where
>     aChoose' :: [Transient] -> Action
>     aChoose' []     = aFail
>     aChoose' [t]    = doB (Tr t)
>     aChoose' (t:ts) = doB (Tr t) `ambN` aChoose' ts

Yes, I know this isn't fair (for a list $[x_1,x_2,\dots,x_n]$,
element $x_i$ is chosen with probability $2^{-i}\mid i<n$, and
probability $2^{-(n-1)}\mid i=n$, rather than uniform probability),
but it's straightforward and easy to code.

> aCheck yy      = yy                              `bindM` \y ->
>                  if (prj1' y "aCheck") then aComplete
>                                        else aFail

> aUnfold        = rdA                             `bindM` \a ->
>                  pauseR a

|aUnfold| doesn't do a |wipeenv|; this is intentional.  However, it does
introduce an interruptible point (a |pauseR|)
(see~\cite[C.3.3.2,~p.~288]{Mosses92:Action}).


\subsubsection{Declarative}
\label{sec:code:actions-declarative}

Now the level-3 actions.  A useful support function, |givenil|, gives no
result.  All declarative actions do this.

> givenil :: Action
> givenil = doB (Tr tnil)

> aBindTo  :: Yielder -> Yielder -> Action
> aUnbind  :: Yielder -> Action
> aRebind  :: Action
> aProduce :: Yielder -> Action

These actions all follow Mosses.

> aBindTo ytok yt = ytok                          `bindM` \tok ->
>                   yt                            `bindM` \t ->
>                   setE (bindTo (prj1' tok "aBindTo") t)
>                                                 `bindM` \() ->
>                   givenil

> aUnbind ytok    = aBindTo ytok (yield unknown)

> aRebind         = givenil

> aProduce ye     = ye                            `bindM` \e ->
>                   setE (makeEnvMap (prj1' e "aProduce"))
>                                                 `bindM` \() ->
>                   givenil


\subsubsection{Imperative}
\label{sec:code:actions-imperative}

The level-4 actions.  A useful support function is |commit|, which
commits us to the current alternative, and also returns a nil result
and no bindings.
All imperative actions commit first.

> commit :: Action
> commit = orX Com     `bindM` \() ->
>          givenil     `bindM` \() ->
>          wipeenv

Now the actions themselves:

> aStoreIn   :: Yielder -> Yielder -> Action
> aUnstore   :: Yielder -> Action
> aReserve   :: Yielder -> Action
> aUnreserve :: Yielder -> Action
> aAllocate  :: Action

These actions all follow Mosses; note that |aAllocate| comes from the
hybrid facet.

> aStoreIn yt yloc = yt                       `bindM` \t ->
>                    yloc                     `bindM` \loc ->
>                    commit                   `bindM` \() ->
>                    getS                     `bindM` \s ->
>                    case updateCell t s
>                           (prj1' loc "aStoreIn") of
>                      Just s' -> setS s'
>                      Nothing -> aFail

For the actions |aUnstore|, |aReserve| and |aUnreserve|, we use a helper
function, |doToStore|:

> doToStore :: (Store -> Loc -> Maybe Store) -> Yielder -> Action

|doToStore| takes a location yielder and an operator that given a store
and a location returns a modified store (or error), and returns the
action that does the appropriate modification on the store, or fails if
there is an error.

> doToStore storeop yloc
>           = yloc                            `bindM` \loc ->
>             commit                          `bindM` \() ->
>             getS                            `bindM` \s ->
>             case (storeop s (prj1' loc "doToStore")) of
>               Just s' -> setS s'
>               Nothing -> aFail

> aUnstore   = doToStore (updateCell uninitialised)

> aReserve   = doToStore reserveCell

> aUnreserve = doToStore unreserveCell

> aAllocate  = commit                         `bindM` \() ->
>              getS                           `bindM` \s ->
>              let loc = chooseFreeCell s in
>              case reserveCell s loc of
>                Just s' -> setS s'           `bindM` \() ->
>                           doB (Tr (inj loc))
>                Nothing -> aFail


\subsubsection{Reflective}
\label{sec:code:actions-reflective}

The reflective action (there is only one):

> aEnact :: Yielder -> Action

This action follows Mosses.

> aEnact ya = ya                 `bindM` \a ->
>             givenil            `bindM` \() ->
>             wipeenv            `bindM` \() ->
>             pauseR (enactAbs (prj1' a "aEnact"))

Note that the abstraction comes from a function defined in
Section~\ref{sec:code:data-miscellaneous}, based on |abstractAct| in
Section~\ref{sec:code:abstractions}.


\subsubsection{Communicative}
\label{sec:code:actions-communicative}

The communicative actions (which are not a strict duplication of Mosses).
Remember, |commit| commits, wipes the environment and gives nothing.
All communicative actions do this.

> aSendData   :: Yielder -> Action
> aRemoveData :: Action

These do \emph{not} follow Mosses' communicative actions. 
|aSendData yt| outputs the transient yielded by |yt|; |aRemoveData|
clears the input buffer.  See also
Section~\ref{sec:code:yielders-communicative}.

> aSendData yt = yt         `bindM` \t ->
>                commit     `bindM` \() ->
>                sendC t

> aRemoveData  = commit     `bindM` \() ->
>                wipebufC


\subsubsection{Directive}
\label{sec:code:actions-directive}

The directive actions:

> aIndirectlyBindTo  :: Yielder -> Yielder -> Action
> aRedirectTo        :: Yielder -> Yielder -> Action
> aUndirect          :: Yielder -> Action
> aRecursivelyBindTo :: Yielder -> Yielder -> Action
> aIndirectlyProduce :: Yielder -> Action

These actions all follow Mosses (but see
Sections~\ref{sec:code:yielders-declarative}
and~\ref{sec:code:yielders-directive}, and also note on the definition of
|aUndirect|).

> aIndirectlyBindTo ytok yt
>   = ytok                            `bindM` \tok ->
>     yt                              `bindM` \t ->
>     getD                            `bindM` \d ->
>     case makeInd d t of
>       Just ~(d',ind) -> setD d' `bindM` \() ->
>                         aBindTo (yield tok) (yieldInj ind)
>       Nothing        -> aFail

> aRedirectTo ytok yt
>   = yDataBoundTo ytok               `bindM` \ind ->
>     yt                              `bindM` \t ->
>     getD                            `bindM` \d ->
>     case redirInd d (prj1' ind "aRedirectTo") t of
>       Just d' -> setD d'            `bindM` \() ->
>                  givenil            `bindM` \() ->
>                  wipeenv
>       Nothing -> aFail

> aUndirect ytok
>   = yDataBoundTo ytok               `bindM` \ind ->
>     getD                            `bindM` \d ->
>     case redirInd d (prj1' ind "aUndirect") unknown of
>       Just d' -> setD d'            `bindM` \() ->
>                  givenil            `bindM` \() ->
>                  wipeenv
>       Nothing -> aFail

Note that we can't use |freeInd| here because we are required to return
\textsf{unknown} and not \textsf{nothing} for an undirected indirection
(see~\cite[p.~311]{Mosses92:Action}).  Unfortunately, this strictly
violates Mosses' specification~\cite[p.~311]{Mosses92:Action}:
``\dots and makes it available for reuse.''

> aRecursivelyBindTo ytok yt
>   = ytok      `bindM` \tok ->
>     indivR
>       ((cFurthermore (aIndirectlyBindTo (yield tok)
>                                         (yield unknown)))
>        `cHence`
>        (aRedirectTo (yield tok) yt `cAnd` aRebind))

The above is based on \cite[p.~270]{Mosses92:Action}, with an obvious
simplification.  Note that it is correct here for |yt| to be affected
by what goes on before.

> aIndirectlyProduce yd
>   = yd                                           `bindM` \d ->
>     setD (makeRedirMap
>             (prj1' d "aIndirectlyProduce"))      `bindM` \() ->
>     givenil                                      `bindM` \() ->
>     wipeenv


\subsubsection{Continuational}
\label{sec:code:actions-continuational}

The continuational facet is an experimental addition to action semantics,
adding first-class continuations.  It requires |ContT|.

> aJump     :: Yielder -> Action
> aJumpWith :: Yielder -> Yielder -> Action

There are two actions: |aJump yk| and |aJumpWith yk yt|.
|yk| yields a continuation, and |yt| yields data.  Note that a
continuation is simply an abstraction that happens to be a continuation,
and in fact |yk| could yield any abstraction.
(Because of this, |aJump| and |aJumpWith| are simply abbreviations,
strictly unnecessary).

The behaviour of |aJump| is to jump to the
continuation yielded by |yk|, passing it the current transient data (and
environment, but if |yk| is purely a continuation this will be ignored).
|aJumpWith| is the same, except that the transient data passed is
that yielded by |yt|.  If for some reason (e.g., the abstraction passed was
not a continuation) control happens to flow past the |aJump|, it
receives the transient data, environment etc.\ coming out of the
continuation.

> aJump yk = aEnact (yClosure (yApplicationTo yk yIt))

> aJumpWith yk yt = aEnact (yClosure (yApplicationTo yk yt))


\subsection{Combinators}
\label{sec:code:combinators}

We also define combinators by facet, again omitting the hybrid facet
(the combinators |cAndThenMoreover|, |cThenMoreover|, |cThence|
and |cThenBefore| are defined with the declarative facet).

\bigskip

First up, we define functions |bincom| and |bincompar| that generalise
the behaviour of the binary combinators.

> bincom ::
>     Action ->                                -- a1
>     (Environment -> Behaviour -> Action) ->  -- link
>     Action ->                                -- a2
>     (Behaviour -> Commitment -> Bool) ->     -- proceed_p
>     (Environment -> Behaviour ->
>      Environment -> Behaviour -> Action)     -- combine
>     -> Action

Executing |bincom a1 link a2 proceed_p combine| does the following:
executes |a1| and then possibly |a2| in the same
initial environment (|Environment| and |Behaviour|),
executing |link e1 b1| just before |a2|.
|a2| is only executed if |proceed_p b1 x1| is |True|;
otherwise |bincom| stops immediately.  After |a2| is
executed, |combine e1 b1 e2 b2| is executed to finish up.
Each subbranch is
executed uncommitted, but the resultant commitment status is the |orCom|
of the commitment of the two branches and the incoming commitment.

> bincompar ::
>     Action ->                                -- a1
>     Action ->                                -- a2
>     (Environment -> Behaviour ->
>      Environment -> Behaviour -> Action)     -- combine
>     -> Action

Executing |bincompar a1 a2 combine| achieves essentially the same thing
as |bincom|,
except that there is no linking between actions and both |a1| and |a2|
are run \emph{in parallel}, stopping execution of both only if one fails
or escapes.

We note here the common uses of the arguments:
\begin{description}
\item[a1 and a2] are the actions to be combined.
\item[link] is used to thread transients and bindings between
  the actions in |cThen| and |cTrap|, among others.
\item[proceed\_p] is used to decide if |a2| should be executed.
  Note that if this fails, |bincom| by default produces the
  environment and transients produced by |a1|.
\item[combine] is sometimes used to combine the environments and
  transients of the two actions.  Note that |bincom| by default produces
  the environment and transients produced by |a2|.
\end{description}

\medskip

First, a useful helper function, |getEBX|:

> getEBX :: M (Environment,Behaviour,Commitment)

> getEBX = getE                         `bindM` \e ->
>          getB                         `bindM` \b ->
>          getX                         `bindM` \x ->
>          unitM (e,b,x)

Now the code for |bincom|.  Note the |pauseR| inserted in between the
two actions.

> bincom a1 link a2 proceed_p combine
>   =
>     getEBX                            `bindM` \(e0,b0,x0) ->
>     unX                               `bindM` \() ->
>     a1                                `bindM` \() ->
>     getEBX                            `bindM` \(e1,b1,x1) ->
>
>     if proceed_p b1 x1
>     then
>       setE e0                         `bindM` \() ->
>       doB b0                          `bindM` \() ->
>       unX                             `bindM` \() ->
>       link e1 b1                      `bindM` \() ->
>       pauseR a2                       `bindM` \() ->
>       getEBX                          `bindM` \(e2,b2,_) ->
>       orX (x0 `orCom` x1)             `bindM` \() ->
>       combine e1 b1 e2 b2
>     else
>       orX x0

And the code for |bincompar|.  The first, commented-out, version is for
use in the sequential version of this program (i.e., without
|ParMMonad|).

Again, note the |pauseR| inserted between the actions.  If this were
not inserted,
then |bincompar m1 m2|, where |m1| and |m2| were both atomic,
would do one monad, then the other, and then combine, all without any
interruption points.

* bincompar a1 a2 combine
*   = bincom a1 noplink a2 complete_p combine

> bincompar a1 a2 combine
>   =
>     getX                              `bindM` \x0 ->
>     unX                               `bindM` \() ->
>     par'P a1 a2 com                   `bindM` \vals ->
>     case vals of
>       Nothing
>         -> orX x0
>       Just (e1,b1,x1,e2,b2)
>         -> orX (x0 `orCom` x1)        `bindM` \() ->
>            combine e1 b1 e2 b2
>
>   where com n m1 m2
>           = m1                        `bindM` \() ->
>             getEBX                    `bindM` \(e1,b1,x1) ->
>             case b1 of
>               Tr t1 -> pauseR m2      `bindM` \() ->
>                        getEBX         `bindM` \(e2,b2,_) ->
>                        case b2 of
>                          Tr t2 -> unitM (Just (case n of
>                                     1 -> (e1,b1,x1,e2,b2)
>                                     2 -> (e2,b2,x1,e1,b1)))
>                          _     -> unitM Nothing
>               _     -> unitM Nothing

In the definition of |com|, remember from
Section~\ref{sec:code:parallelism-monad} that |m1| and |m2|
already know their values for all features above |ResT|, i.e., all
values that may be different between threads.  As noted 
in Section~\ref{sec:code:combined-monad}, $EBX$
must fall into this category, and so |m1| and |m2| `know' their $EBX$
values already.  Hence there is no need to restore the initial state
before calling |m2|.

\medskip

Support functions for combinators using the above: 
|complete_p| tests if the action
completed, |escape_p| tests if the action escaped.

> complete_p, escape_p :: Behaviour -> Commitment -> Bool

> complete_p (Tr _)  _ = True
> complete_p _       _ = False

> escape_p   (Esc _) _ = True
> escape_p   _       _ = False

> noplink    :: Environment -> Behaviour -> Action
> nopcombine :: Environment -> Behaviour ->
>               Environment -> Behaviour -> Action

|noplink| and |nopcombine| don't link anything and don't combine
anything, respectively.  Specifically, they enable the default to happen:
|a2| is performed in the same environment as |a1|, and the result of the
combination is the result of |a2|.

> noplink _ _ = nop

> nopcombine _ _ _ _ = nop

> disjunenv    :: Environment -> Environment -> Action
> tupleonly    :: Behaviour -> Behaviour -> Action
> disjandtuple :: Environment -> Behaviour ->
>                 Environment -> Behaviour -> Action

|disjunenv| combines the two environments if they don't
conflict (forming their disjoint union), else it fails.
|tupleonly| tuples the transients if both actions succeed, else it does
nothing (and allows |a2|'s results to fall through).
|disjandtuple|, as its name suggests, forms
the disjoint union of the two environments \emph{and} tuples the transients if
both actions succeed, else it does nothing (and allows |a2|'s results to
fall through).

> disjunenv e1 e2
>   = if isConflict e1 e2
>     then aFail
>     else setE (overlay e1 e2)

> tupleonly b1 b2
>   = case (b1,b2) of
>       (Tr t1, Tr t2) -> doB (Tr (tcons t1 t2))
>       _              -> nop

> disjandtuple e1 b1 e2 b2
>   = case (b1,b2) of
>       (Tr t1, Tr t2) -> doB (Tr (tcons t1 t2))   `bindM` \() ->
>                         disjunenv e1 e2
>       _              -> nop

And some functions for the declarative facet:

> overlaybs    :: Environment -> Environment -> Action
> overandtuple :: Environment -> Behaviour ->
>                 Environment -> Behaviour -> Action

|overlaybs| overlays the two environments, preferring the second.  It
does not affect the transients, allowing the second action's transients
to fall though.
|overandtuple| overlays the two environments and tuples the transients.

> overlaybs e1 e2
>   = setE (overlay e1 e2)

> overandtuple e1 b1 e2 b2
>   = case (b1,b2) of
>       (Tr t1, Tr t2) -> doB (Tr (tcons t1 t2))   `bindM` \() ->
>                         overlaybs e1 e2
>       _              -> nop


\subsubsection{Basic and Functional}
\label{sec:code:combinators-basic-and-functional}

We build the combinators of the basic and functional facets,
on top of the monad.  Note that the combinators are all declared
|infixl|, i.e., left-associative: |a `cThen` b `cThen` c| is
|(a `cThen` b) `cThen` c|, and is not the other possibility,
|a `cThen` (b `cThen` c)|.

\medskip

The combinators themselves:

> cOr, cThen, cAndThen, cAnd, cTrap :: Action -> Action -> Action
> cUnfolding :: Action -> Action
> infixl `cOr`, `cThen`, `cAndThen`, `cAnd`, `cTrap`

These combinators all follow Mosses.

> a1 `cOr` a2 = (cOr' a1 a2) `ambN` (cOr' a2 a1)
>   where
>     cOr' a1 a2 = bincom a1  noplink  a2
>                         (\b1 x1 -> (b1,x1)==(Fail,Unc))
>                         nopcombine

Note that |cOr| does either |a1| then |a2|, or |a2| then |a1|,
nondeterministically, trying the other only if the first fails without
committing.

> a1 `cThen` a2
>   = bincom a1  (\_ b1 -> doB b1)  a2
>            complete_p  (\e1 _ e2 _ -> disjunenv e1 e2)

> a1 `cAndThen` a2
>   = bincom a1  noplink  a2
>            complete_p  disjandtuple

> a1 `cAnd` a2
>   = bincompar a1 a2 disjandtuple

> a1 `cTrap` a2
>   = bincom a1  (\_ (Esc t1) -> aGive (yield t1))  a2
>            escape_p  nopcombine

> cUnfolding a
>   = withA a a

Note how the |UnfoldT| (see Section~\ref{sec:code:bf-monad-transformer})
environment is used to store the action to unfold.

> cIndivisibly a = indivR a


\subsubsection{Declarative}
\label{sec:code:combinators-declarative}

Now the level-3 combinators.

> cFurthermore               :: Action -> Action
> cMoreover, cHence, cBefore :: Action -> Action -> Action
> infixl `cMoreover`, `cHence`, `cBefore`

These combinators all follow Mosses.

> cFurthermore a
>   = getE                  `bindM` \e0 ->
>     a                     `bindM` \() ->
>     getE                  `bindM` \e1 ->
>     setE (overlay e0 e1)

> a1 `cMoreover` a2
>   = bincompar a1 a2 overandtuple

> a1 `cHence` a2
>   = bincom a1  (\e1 _ -> setE e1)  a2
>            complete_p  (\_ b1 _ b2 -> tupleonly b1 b2)

> a1 `cBefore` a2
>   = bincom a1  link  a2
>            complete_p  overandtuple
>       where
>         link e1 _
>           = getE                   `bindM` \e0 ->
>             setE (overlay e0 e1)

The combinators from the hybrid `facet' rightfully belong here also:

> cAndThenMoreover, cThenMoreover, cThence, cThenBefore ::
>    Action -> Action -> Action
> infixl `cAndThenMoreover`, `cThenMoreover`,
>        `cThence`, `cThenBefore`

> a1 `cAndThenMoreover` a2
>   = bincom a1  noplink  a2
>            complete_p  overandtuple

> a1 `cThenMoreover` a2
>   = bincom a1  (\_ b1 -> doB b1)  a2
>            complete_p  (\e1 _ e2 _ -> overlaybs e1 e2)

> a1 `cThence` a2
>   = bincom a1  link  a2
>            complete_p  (\e1 _ e2 _ -> disjunenv e1 e2)
>       where
>         link e1 b1
>           = doB b1                `bindM` \() ->
>             setE e1


> a1 `cThenBefore` a2
>   = bincom a1  link  a2
>            complete_p  (\e1 _ e2 _ -> disjunenv e1 e2)
>       where
>         link e1 b1
>           = doB b1                `bindM` \() ->
>             getE                  `bindM` \e0 ->
>             setE (overlay e0 e1)


\subsubsection{Communicative}
\label{sec:code:combinators-communicative}

The communicative combinator.

> cPatiently :: Action -> Action

This combinator follows Mosses.

> cPatiently a = getB                              `bindM` \b0 ->
>                getE                              `bindM` \e0 ->
>                cUnfolding
>                  (indivR a                       `bindM` \() ->
>                   getB                           `bindM` \b ->
>                   case b of
>                     Fail -> doB b0               `bindM` \() ->
>                             setE e0              `bindM` \() ->
>                             aUnfold
>                     _    -> nop)

We don't need a |pauseR| on |aUnfold|, since it does it itself.


\subsubsection{Continuational}
\label{sec:code:combinators-continuational}

The continuational combinator.  This facet is an experimental addition
to action semantics (see Section~\ref{sec:code:actions-continuational}).

> cWithCC :: Yielder -> Action -> Action

|cWithCC ytok a| does action |a| providing the transients received
by |cWithCC| and in an environment consisting of the
environment passed to |cWithCC|, extended with a binding of the
token yielded by |ytok| to the continuation of the |cWithCC ytok a|
statement.  Note that a continuation is merely an abstraction that when
enacted happens to cause execution to resume from the point at which
|cWithCC| was called.  Transients are passed through this `wormhole',
but environments and other data above |ContT| are not.

If |a|
executes normally (i.e., doesn't jump out), then |cWithCC| yields the
same transients and environment that |a| does.  If the |cWithCC| is
later jumped to, the transients yielded will be those passed to
|aJump|, but the environment yielded will be that passed to |cWithCC|
originally (as will the commitment status).

> cWithCC ytok a
>   = ytok                                     `bindM` \tok ->
>     callccK (\k ->
>       getE                                   `bindM` \e ->
>       setE (overlay e
>              (bindTo (prj1' tok "cWithCC")
>                      (inj (abstractAct
>                             (getB            `bindM` \(Tr t) ->
>                              k t             `bindM` \t' ->
>                              doB (Tr t'))))))
>                                              `bindM` \() ->
>       a                                      `bindM` \() ->
>       getB                                   `bindM` \b ->
>       unitM (case b of
>                Tr t -> t
>                _    -> tnil))                `bindM` \t ->
>     getB                                     `bindM` \b ->
>     case b of
>       Tr _ -> doB (Tr t)
>       _    -> nop

Note the special handling required: if |a| fails or escapes, we mustn't
destroy this information.  Hence we check for it outside the
continuation, \emph{first}, before we set the return transient of the
|cWithCC|; if the action has failed or escaped, we simply allow this
situation to fall through.  Note that this can only be caused by |a|
failing or escaping; if it had happened before we got to |cWithCC|,
we wouldn't have got \emph{to} |cWithCC|.

Within the |callccK|, note firstly that to get to the |getB|, we must be
complete rather than escaped or failed, and so the pattern match is
legal; secondly, |k| here is a `real' continuation, provided by
|callccK|, and hence it always does the right thing (i.e., if it returns,
it is complete rather than escaped or failed; but of course it never
returns in this case) and so we can simply use |doB (Tr t')| here (in
fact, |nop| would do fine, since the |k t| will never return).



\subsection{Yielders}
\label{sec:code:yielders}

We also need some yielders.  These are used slightly differently from
how they would be used in Mosses' AS, and hence we must be careful in
the definitions not to modify any state, just to read it.

Yielders are defined by facet also.

In Mosses, yielders are constrained to be `read-only'---they change
nothing, only examining the state and returning a transient.  Our system
does not enforce this (yielders are monads instantiated over
|Transient|), and so we must be very careful to impose this restriction
on ourselves.

Note also, we must be careful when using yielders that we evaluate them
before changing any state on which they might depend.  This means that
if we are defining an action taking yielders as arguments, we should
evaluate the yielders immediately, even if we want to pass them on to
another action that also takes yielders.  Consider the error in the
following:

\begin{verbatim}
  aJumpWith yk yt = aGive yt `cThen` aJump yk
\end{verbatim}

If we do |aJumpWith (yieldInj 42) yIt|, the above definition will fail
miserably.  Instead, we must evaluate both |yk| and |yt|, give |yt|, and
then jump to |yield k|.


\subsubsection{Basic and Functional}
\label{sec:code:yielders-basic-and-functional}

The basic and functional yielders.

> yIt :: Yielder
> yGivenN :: Yielder -> Yielder

|yIt| yields the given data (not just datum).
|yGivenN n| yields the |n|th element of the passed tuple.

> yIt = getB     `bindM` \~(Tr x) ->
>       unitM x

We can use this pattern here because a yielder will never be
called on a failed action: if the previous action has failed, then
execution will stop instead.  Hence we know when we come into a yielder
that the current |Behaviour| is `complete', or |Tr _|.

> yGivenN yn = yIt                                  `bindM` \x ->
>              yn                                   `bindM` \n ->
>              let xs = prj1' x "yGivenN - x" :: [Transient]
>                  i  = (prj1' n "yGivenN - i")
>              in unitM (xs `safeInd` i)
>   where
>     safeInd xs i = if i>0 then safeInd' xs i
>                           else tnil
>     safeInd' (x:xs) 1     = x
>     safeInd' (x:xs) (n+1) = safeInd' xs n
>     safeInd' []     _     = tnil

We follow here \cite[p.~321]{Mosses92:Action}: the index must be
positive, otherwise (or if there are not enough elements in the tuple)
\textsf{nothing} is returned.


\subsubsection{Declarative}
\label{sec:code:yielders-declarative}

And the level-3 yielders:

> yCurrentBindings :: Yielder
> yDataBoundTo     :: Yielder -> Yielder
> yReceiving       :: Yielder -> Yielder -> Yielder

These yielders follow Mosses, except that |yDataBoundTo| will return an
indirection rather than the actual data if it is used on an indirection.
This is an unavoidable consequence of the data model I am using;
however, see |yDataIndBoundTo| (Section~\ref{sec:code:yielders-directive}).

> yCurrentBindings   = getE                       `bindM` \e ->
>                      unitM (inj (getEnvMap e))

> yDataBoundTo ytok  = ytok                       `bindM` \tok ->
>                      getE                       `bindM` \e ->
>                      unitM (case lookup
>                                    (prj1' tok "yDataBoundTo")
>                                    e of
>                               Just v  -> v
>                               Nothing -> tnil)

> y1 `yReceiving` y2 = y2                         `bindM` \e ->
>                      getE                       `bindM` \e0 ->
>                      setE (makeEnvMap (prj1' e "yReceiving"))
>                                                 `bindM` \() ->
>                      y1                         `bindM` \x ->
>                      setE e0                    `bindM` \() ->
>                      unitM x

Note that we must not modify the environment in which |f| executes;
hence we save and restore it around the execution of |y1|.  Note also
that the fact that |y1| here is evaluated in a different environment to
the whole expression is obviously correct for the intended behaviour of
|yReceiving|.


\subsubsection{Imperative}
\label{sec:code:yielders-imperative}

The level-4 yielders:

> yCurrentStorage :: Yielder
> yDataStoredIn   :: Yielder -> Yielder

These follow Mosses.

> yCurrentStorage  = getS                         `bindM` \s ->
>                    unitM (inj (getStoreMap s))

> yDataStoredIn y1 = y1                           `bindM` \loc ->
>                    getS                         `bindM` \s ->
>                    unitM (case readCell s
>                                  (prj1' loc "yDataStoredIn") of
>                             Just t  -> t
>                             Nothing -> tnil)


\subsubsection{Reflective}
\label{sec:code:yielders-reflective}

The reflective yielders.

> yApplicationTo :: Yielder -> Yielder -> Yielder
> yClosure       :: Yielder -> Yielder

The reflective yielders follow Mosses.

> yApplicationTo ya yt = ya                        `bindM` \a ->
>                        yt                        `bindM` \t ->
>                        unitM (inj (abstractAct
>                               (doB (Tr t)        `bindM` \() ->
>                                enactAbs
>                                  (prj1' a "yApplicationTo") )))

> yClosure ya          = ya                        `bindM` \a ->
>                        getE                      `bindM` \e ->
>                        unitM (inj (abstractAct
>                               (setE e            `bindM` \() ->
>                                enactAbs
>                                  (prj1' a "yClosure") )))


\subsubsection{Communicative}
\label{sec:code:yielders-communicative}

The communicative yielders.

> yCurrentBuffer :: Yielder

Only one of Mosses' three communicative yielders is defined.
The yielder |yCurrentBuffer| allows access to the contents of the input buffer.
Note that (as mentioned in Section~\ref{sec:code:communications}) this
yielder (incorrectly) \emph{blocks} if the buffer is empty, until input
is received.

There are two other yielders that are omitted: |yPerformingAgent| and
|yContractingAgent|.  In a single-agent system like this one, these do
not make sense.

> yCurrentBuffer = getbufC                   `bindM` \buf ->
>                  unitM (case buf of
>                           Just t  -> t
>                           Nothing -> tnil)


\subsubsection{Directive}
\label{sec:code:yielders-directive}

The directive yielders.

> yCurrentRedirections :: Yielder
> yIndirectClosure     :: Yielder -> Yielder
> yDataIndBoundTo      :: Yielder -> Yielder

The yielders |yCurrentRedirections| and |yIndirectClosure| follow Mosses;
the new yielder |yDataIndBoundTo| does what |yDataBoundTo|
(Section~\ref{sec:code:yielders-declarative}) is supposed to
do once we add the directive facet:
transparently dereference indirections if necessary.

> yCurrentRedirections = getD                      `bindM` \d ->
>                        unitM (inj (getRedirMap d))

> yIndirectClosure ya 
>     = ya                                         `bindM` \a ->
>       getD                                       `bindM` \d ->
>       unitM (inj (abstractAct
>                     (setD d                      `bindM` \() ->
>                      enactAbs (prj1' a "yIndirectClosure") )))

> yDataIndBoundTo ytok
>     = ytok                                      `bindM` \tok ->
>       getE                                      `bindM` \e ->
>       getD                                      `bindM` \d ->
>       unitM (case lookup (prj1' tok "yDataIndBoundTo") e of
>                Just v  -> case prj v of
>                             Just ind -> case readInd ind d of
>                                           Just t  -> t
>                                           Nothing -> tnil
>                             Nothing  -> v
>                Nothing -> tnil)


\subsection{Data}
\label{sec:code:data}

There are a large number of operators on data in Mosses' action
semantics.  In our system, these appear as yielders; however their
result depends only on the values of their arguments, not on any
information carried by the monad.

These operators are defined in this section.  Since they do not depend
on the monad information, they can all be defined first as |yFoo_| from
|Transient|${}^n$ to |Transient|, before being lifted to |yFoo| from
|Yielder|${}^n$ to |Yielder|.

\subsubsection{Machinery}
\label{sec:code:data-machinery}

The functions in this section allow us to convert Gofer primitives into
functions on |Transient|s, and then to functions on |Yielder|s.

\medskip

First up, we define |yield| and |yieldInj|, which turn constants into
yielders of that constant.  These of course do not appear in Mosses,
but are necessitated here by the different type system we use.

> yield :: Transient -> Yielder

> yield t = unitM t

|yieldInj| combines this with |inj|, so that primitive data can be
|yield|ed easily.

> yieldInj x = yield (inj x)

Now some operations for lifting functions from primitive types to
the union type |Transient|.

> lift1ToTransient  :: (SubType a Transient,
>                       SubType b Transient) =>
>   (a -> b) -> (Transient -> Transient)

> lift1tToTransient :: (SubType a [Transient],
>                       SubType b Transient) =>
>   (a -> b) -> (Transient -> Transient)

> lift2ToTransient  :: (SubType a Transient,
>                       SubType b Transient,
>                       SubType c Transient) =>
>   (a -> b -> c) -> (Transient -> Transient -> Transient)

|lift1ToTransient| takes a unary function from |a|
to |b| (both simple types) to a function from |Transient| to |Transient|.
|lift1tToTransient| takes a unary function from |[a]| to |b| 
to a function from |Transient| to |Transient|.
|lift2ToTransient| takes a binary function from |a| to |b| to |c| 
to a function from |Transient| to |Transient| to |Transient|.

> lift1ToTransient op x1 = f (prj x1) where
>   f (Just n1) = inj (op n1)
>   f Nothing   = tnil

> lift1tToTransient op x1 = f (prj x1::Maybe [Transient]) where
>   f Nothing   = tnil
>   f (Just n1) = g (prj n1) where
>     g (Just p1) = inj (op p1)
>     g Nothing   = tnil

> lift2ToTransient op x1 x2 = f (prj x1) (prj x2) where
>   f (Just n1) (Just n2) = inj (op n1 n2)
>   f _ _                 = tnil

Now we need to lift the functions from |Transient|s to |Yielder|s.

> lift1ToYielder :: (Transient -> Transient)
>                     -> (Yielder -> Yielder)
> lift2ToYielder :: (Transient -> Transient -> Transient)
>                     -> (Yielder -> Yielder -> Yielder)

> lift1ToYielder op y1
>   = y1        `bindM` \x1 ->
>     unitM (op x1)

> lift2ToYielder op y1 y2
>   = y1        `bindM` \x1 ->
>     y2        `bindM` \x2 ->
>     unitM (op x1 x2)


\subsubsection{Miscellaneous}
\label{sec:code:data-miscellaneous}

> yPredecessorOf_ = lift1ToTransient (+ (-1::Int))
> yNot_           = lift1ToTransient not

> yProductOf_     = lift1tToTransient (foldl (*) (1::Int))
> ySumOf_         = lift1tToTransient (foldl (+) (0::Int))

> yIsLessThan_    = lift2ToTransient  ((<)::Int->Int->Bool)
> yIsGreaterThan_ = lift2ToTransient  ((>)::Int->Int->Bool)
> yIsEqualTo_     = lift2ToTransient ((==)::Int->Int->Bool)
> yIsNotEqualTo_  = lift2ToTransient ((/=)::Int->Int->Bool)

> yPairOf_ :: Transient -> Transient -> Transient
> yPlus_   :: Transient -> Transient -> Transient

> yPairOf_ x y = inj ([x,y])

> yPlus_ t1 t2 = inj (prj1 t1 + prj1 t2 :: Int)

> yCount_  :: Transient -> Transient
> yFirst_  :: Transient -> Transient
> yRest_   :: Transient -> Transient

> yCount_ t = inj (length (prj1 t::[Transient]))

> yFirst_ t = case (prj1' t "yFirst_")::[Transient] of
>               t':_ -> t'
>               []   -> tnil

> yRest_ t  = case (prj1' t "yRest_")::[Transient] of
>               _:ts -> inj ts
>               []   -> tnil

The following operations are required for the reflective facet to be of
any use.

> yAbstractionOf_ :: Action -> Transient
> yProvision_     :: Transient -> Transient
> yProduction_    :: Transient -> Transient

|yAbstractionOf| converts an action into an abstraction.  |yProvision|
creates an abstraction that gives data; |yProduction| creates an
abstraction that produces bindings.

> yAbstractionOf_ a = inj (abstractAct a)

> yProvision_ t     = inj (abstractAct (doB (Tr t)))

> yProduction_ t    = inj (abstractAct
>                            (setE (makeEnvMap (prj1 t))))


\subsubsection{Final liftings}
\label{sec:code:data-final-liftings}

We lift our functions up to yielders finally.

> yPredecessorOf = lift1ToYielder yPredecessorOf_
> yNot           = lift1ToYielder yNot_
> yProductOf     = lift1ToYielder yProductOf_
> ySumOf         = lift1ToYielder ySumOf_
> yIsLessThan    = lift2ToYielder yIsLessThan_
> yIsGreaterThan = lift2ToYielder yIsGreaterThan_
> yIsEqualTo     = lift2ToYielder yIsEqualTo_
> yIsNotEqualTo  = lift2ToYielder yIsNotEqualTo_
> yPairOf        = lift2ToYielder yPairOf_
> yPlus          = lift2ToYielder yPlus_
> yCount         = lift1ToYielder yCount_
> yFirst         = lift1ToYielder yFirst_
> yRest          = lift1ToYielder yRest_
> yProvision     = lift1ToYielder yProvision_
> yProduction    = lift1ToYielder yProduction_
> yAbstractionOf = yield . yAbstractionOf_

\ifstandalone
\bibliography{keith}
\fi