%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%                                                         %%%%%%%%%%
%%%%%%%%%%     Idiomatica                                          %%%%%%%%%%
%%%%%%%%%%                                                         %%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass{article}
\usepackage{stmaryrd}
\usepackage{named}
%include lhs2TeX.fmt 
%include lhs2TeX.sty 
\DeclareMathAlphabet{\mathkw}{OT1}{cmss}{bx}{n}

%subst keyword a = "\mathkw{" a "}"
%subst conid a = "\mathsf{" a "}"

%format $ = "\mathbin{\mbox{\small\$}}"
%format <*> = "\circledast"
%format <$> = "\mathop{\mbox{\(\left<\!\mbox{\small\$}\!\right>\)}}"
%format *> = "\mathop{\mbox{\(*\!\!\!\!>\)}}"
%format <* = "\mathop{\mbox{\(<\!\!\!\!*\)}}"
%format iI = "\llbracket"
%format Ii = "\rrbracket"
%format Ig = "\dagger\!\!"
%format Pu = "{}^{\natural}\!\!"
%format Ji = "\rrbracket\hspace*{-0.04in}\raisebox{-0.03in}{\({}_" J "\)}"
%format un (x) = "\left\lfloor" x "\right\rfloor"
%format op x = x "^\circ"
%format zero = "\emptyset"
%format <+>  = "\oplus"
%format Zero = "\mathsf{0}"
%format Sum p q = p "+" q
%format Prod p q = p "\times" q
%format :*: = "\mathbin{:\!\!\times\!\!:}"
%format Compo p q = p "\circ" q
%format <+ = "\mathop{<\!\!\!\!+}"
%format Mo (ls) (i) (s) (o) (e) (m) = "\left<" ls "|" i "/" s "/" o "\!\uparrow\!" e "\right>_{" m"}"
%format ?= = "\mathop{?\!\!=}"
%format \= = "\mathop{\backslash\!\!=}"
%format != = "\mathop{!\!\!=}"



\parindent 0in
\parskip 0.1in


\begin{document}
\title{Idiomatica}
\author{Conor McBride}
\maketitle

\section{Introduction}

%if False

> {-# OPTIONS -fglasgow-exts -fallow-overlapping-instances -fallow-undecidable-instances #-}

> module Idiomatica where

> import Prelude hiding (foldl, foldr)
> import Control.Monad
> import Data.Set
> import Data.Either
> import Control.Applicative
> import Data.Monoid hiding (Sum)
> import Data.Foldable
> import Data.Traversable
> import qualified GHC.Prim as P 

%endif

Based on the ideas presented in~\cite{conor.ross:applicative},
|Control.Applicative| and |Data.Traversable| are now to be found in the
Standard Library. This module delivers a collection of goodies which go
further.

This stuff is quite experimental. A number of changes could make it cleaner.
For example, Ashley Yakeley's |Functor| hierarchy proposal would remove a lot
of unfortunate duplication.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Applicative Functors}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We take the following definition of an \emph{applicative functor}:

< class Applicative f where
<   -- Lift a value.
<   pure :: a -> f a
<
<   -- Sequential application.
<   (<*>) :: f (a -> b) -> f a -> f b
<
<   -- Map a function over an action.
<   (<$>) :: (a -> b) -> f a -> f b
<   f <$> v = pure f <*> v


We also acquire the operations which sequence effects but discard values.

< (*>) :: Applicative f => f a -> f b -> f b
< (<*) :: Applicative f => f a -> f b -> f a

It's sometimes useful to have a flipped |<$>| for infix stuff.

> (<~$>) :: Applicative f => f a -> (a -> b) -> f b
> (<~$>) = flip (<$>)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Idiom Brackets}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


Next, we get the `idiom brackets'. This code is a bit cheeky, and it looks
a bit weird in \LaTeX. The basic idea is to disguise

< pure f <*> s1 <*> ... <*> sn

as

< iI f s1 ... sn Ii

so that the idiomatic application has the normal syntax, inside the bracket.

The implementation is a nasty type class hack.

> class Applicative i => Idiomatic i f g | g -> f i where
>   idiomatic :: i f -> g

> iI :: Idiomatic i f g => f -> g
> iI = idiomatic . pure

> data Ii  =  Ii

> instance Applicative i    => Idiomatic i x (Ii -> i x) where
>   idiomatic xi Ii     = xi
> instance Idiomatic i f g  => Idiomatic i (s -> f) (i s -> g) where
>   idiomatic sfi si    = idiomatic (sfi <*> si)

Now, once we've gone that far, why not go further? We can have add
computations whose effects are sequenced but whose values are ignored.
This is quite useful for adding punctuation in parsers, etc.

> data Ig  =  Ig

> instance Idiomatic i f g  => Idiomatic i f (Ig -> i x -> g) where
>   idiomatic fi Ig xi  = idiomatic (fi <* xi)

Another possibility, given that these things don't nest (grrr), is to mark
pure things as pure. This just saves a bit of bracketing.

> data Pu = Pu

> instance Idiomatic i f g => Idiomatic i (x -> f) (Pu -> x -> g) where
>   idiomatic fi Pu x = idiomatic (fi <*> pure x)

We can also add conditions of type |Bool| to bracketed expressions if we're
working in a |Monoid|. Failure of the condition results in the expression
returning the |zero|.

> data If  =  If

> instance (Idiomatic i f g, Monoid g) => Idiomatic i f (If -> Bool -> g) where
>   idiomatic fi If True   = idiomatic fi
>   idiomatic fi If False  = zero

If our |Applicative| functor happens also to be a |Monad|,
we can insert |join|s wherever we like, so that

< s >>= f

becomes

< iI f s J Ii

Note that if a computation returns functional values, we can carry on
after the |J|, as in this example, where we look up a function from an
environment.

< do  var  <- maybeVar
<     gam  <- maybeEnv
<     fun  <- lookup var gam
<     arg  <- maybeArg
<     return (fun arg)

becomes

< iI lookup maybeVar maybeEnv J maybeArg Ii

> data J   = J

> instance (Monad i, Idiomatic i f g) => Idiomatic i (i f) (J -> g) where
>   idiomatic fii J = idiomatic (join fii)

Even so, |J| is very common at the end, so we have


> data Ji = Ji

> instance (Monad i, Applicative i)    => Idiomatic i (i x) (Ji -> i x) where
>   idiomatic xii Ji = join xii


A little friend for infix things:

> ii :: Applicative i => i r -> (r -> s -> t) -> i s -> i t
> ii ir f is = f <$> ir <*> is


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Traversable Functors}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

By way of a reminder, the interface to |Traversable| consists of just this:

< class Traversable t where
<   -- Map each element of a structure to an action, evaluate
<   -- these actions from left to right, and collect the results.
<   traverse :: Applicative f => (a -> f b) -> t a -> f (t b)

Many of our favourite structures are |Traversable|, eg

< instance Traversable [] where
<   traverse f []        = iI [] Ii
<   traverse f (x : xs)  = iI (:) (f x) (traverse f xs) Ii

It's always the corner cases which get left out of the library.

> instance Foldable (Const k) where
>   foldMap = foldMapDefault

> instance Traversable (Const k) where
>   traverse f (Const k) = iI (Const k) Ii


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Adverbial Programming}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The following type class is intended to bring some uniformity to the business
of forgetting structure. Every |newtype| should give an instance of |Unpack|.


> class Unpack p u | p -> u where
>   un :: p -> u


Now we may have an infix operator whose effect is to `compute' the inverse of
its first argument.

> op :: Unpack p u => (u -> p) -> p -> u
> op _ p = un p

Moreover, we may give a packer \emph{adverbial} force in higher-order
programming, leaving the machine to find the unpacker.

> ily :: Unpack p' u' => (u -> p)  -> (  (t -> p)  -> t'  -> p')
>                                  ->    (t -> u)  -> t'  -> u'
> ily up transformer f t = un (transformer (up . f) t)

> instance Unpack Any Bool where
>   un = getAny

> instance Unpack All Bool where
>   un = getAll


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Monoid Equipment}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Monoids are too useful and too general a notion to be saddled with |mempty|
and |mappend| as methods. Correspondingly, let us have better names to use,
even if we cannot change the names for definitional purposes.

> instance Monoid Bool where
>   mempty = False
>   a `mappend` b = a || b

> infixr 4 <+>
> zero   ::  Monoid x => x
> zero   =   mempty
> (<+>)  ::  Monoid x => x -> x -> x
> (<+>)  =   mappend

We shall get some effort out of these friends:

< instance Monoid b => Monoid (a -> b) where
<   mempty       = iI zero Ii
<   mappend f g  = iI (<+>) f g Ii

There's plenty of other heavy lifting going on. Ross has added 

< instance Monoid m => Applicative (Const m) where
<   pure _              = Const zero
<   Const f <*> Const v = Const (f <+> v)

so now we need merely say things like

%if False

> instance Unpack (Const a b) a where
>   un (Const a) = a
> instance Unpack (Endo x) (x -> x) where
>   un (Endo f) = f

%endif

> crush    ::  (Monoid b, Traversable t) => (a -> b) -> t a -> b
> crush    =   Const `ily` traverse

> combine  ::  Traversable t => (a -> b -> b) -> t a -> b -> b
> combine  =   Endo `ily` crush

While we're here, let's have

> always :: Traversable f => (x -> Bool) -> f x -> Bool
> always p = (All `ily` crush) p

> ever :: Traversable f => (x -> Bool) -> f x -> Bool
> ever p = (Any `ily` crush) p

We should, of course, remember that

> instance Monoid m => Monoid (Const m x) where
>   mempty                       = Const zero
>   mappend (Const x) (Const y)  = Const (x <+> y)

and

< instance Monoid (Maybe x) where
<   mempty                 = Nothing
<   mappend x@(Just _)  _  = x
<   mappend _           y  = y

Locally, we may presume

> instance Monoid Int where
>   mempty   = 0
>   mappend  = (+)

> count :: Traversable t => (a -> Bool) -> t a -> Int
> count p = crush $ \x -> if p x then 1 else 0


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Polynomial Functors}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

I now introduce apparatus for working with polynomials. They're the basic
building blocks of data structures, and they have all sorts of good
properties.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{|Id|}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

The identity functor is monadic, applicative, traversable, etc:

> newtype Id x = Id x
> instance Unpack (Id x) x where
>   un (Id x) = x

> instance Functor Id where
>   fmap f (Id s)  = Id (f s)
> instance Monad Id where
>   return      = Id
>   Id x >>= f  = f x
> instance Applicative Id where
>   pure           = Id
>   Id f <*> Id s  = Id (f s)
> instance Foldable Id where
>   foldMap = foldMapDefault
> instance Traversable Id where
>   traverse f (Id x) = iI Id (f x) Ii

|Id| acts as the variable in polynomial expressions. Meanwhile, constants
are given by |Const k|. However, a particular constant is conspicuous by
its absence.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{|Zero|}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


I still don't like the name |Void| for this thing, so I'm calling it |Zero|.

> newtype Zero = Zero {naughty :: forall a. a}

> inflate :: Functor f => f Zero -> f a
> inflate = P.unsafeCoerce#


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{|Sum|}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


> data (Sum p q) x = Inl (p x) | Inr (q x)

> instance (Functor p, Functor q) => Functor (Sum p q) where
>   fmap f (Inl px) = Inl (fmap f px)
>   fmap f (Inr qx) = Inr (fmap f qx)

> instance (Foldable p, Foldable q) => Foldable (Sum p q) where
>   foldMap f (Inl px) = foldMap f px
>   foldMap f (Inr qx) = foldMap f qx

> instance (Traversable p, Traversable q) => Traversable (Sum p q) where
>   traverse f (Inl px) = iI Inl (traverse f px) Ii
>   traverse f (Inr qx) = iI Inr (traverse f qx) Ii

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Products}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


> infixr 3 :*:
> data (Prod p q) x = p x :*: q x

> instance (Functor p, Functor q) => Functor (Prod p q) where
>   fmap f (px :*: qx) = fmap f px :*: fmap f qx

> instance (Foldable p, Foldable q) => Foldable (Prod p q) where
>   foldMap f (px :*: qx) = foldMap f px <+> foldMap f qx

> instance (Traversable p, Traversable q) => Traversable (Prod p q) where
>   traverse f (px :*: qx) = iI (:*:) (traverse f px) (traverse f qx) Ii

> instance (Applicative p, Applicative q) => Applicative (Prod p q) where
>   pure x                       = pure x       :*: pure x
>   (pf :*: qf) <*> (ps :*: qs)  = (pf <*> ps)  :*: (qf <*> qs)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Composition}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Applicativity is closed under composition:


> newtype (Compo p q) x = Comp (p (q x))
> instance Unpack (Compo p q x) (p (q x)) where
>   un (Comp x) = x

> instance (Functor p, Functor q) => Functor (Compo p q) where
>   fmap f (Comp pqx) = Comp (fmap (fmap f) pqx)

> instance (Foldable p, Foldable q) => Foldable (Compo p q) where
>   foldMap f (Comp pqx) = foldMap (foldMap f) pqx

> instance (Traversable p, Traversable q) => Traversable (Compo p q) where
>   traverse f (Comp pqs) = iI Comp (traverse (traverse f) pqs) Ii

> instance (Applicative p, Applicative q) => Applicative (Compo p q) where
>   pure = Comp . pure . pure
>   Comp pqf <*> Comp pqs = Comp (iI (<*>) pqf pqs Ii)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Napierian Structure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

A |Napierian| functor is one which may faithfully be repesented as
a function from a type of `positions', which we call its `logarithm'.
Such a thing is necessarily |Applicative| with the |(->) l| behaviour.

> class Applicative f => Napierian f l where
>   positions  :: f l
>   proj       :: f x -> l -> x
>   tabulate   :: (l -> x) -> f x
>   tabulate f = iI f positions Ii

The trivial instance which illustrates the idea is the functional
representation of \emph{functions}!

> instance Napierian ((->) l) l where
>   positions  = id
>   proj       = id

Well loved laws of logarithms are as we might hope.

> instance Napierian (Const ()) Zero where
>   proj _ z   = naughty z
>   positions  = zero

> instance (Napierian p l, Napierian q r) =>
>   Napierian (Prod p q) (Either l r) where
>   proj (px :*: qx) (Left l)   = px `proj` l
>   proj (px :*: qx) (Right r)  = qx `proj` r
>   positions = iI Left positions Ii :*: iI Right positions Ii

> instance Napierian Id () where
>   proj (Id x) _  = x
>   positions      = Id ()

> instance (Napierian p x, Napierian q y) =>
>   Napierian (Compo p q) (x, y) where
>   proj (Comp pqx) (x, y)  = pqx `proj` x `proj` y
>   positions =
>     iI (,) (Comp (iI pure positions Ii)) (Comp (pure positions)) Ii


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Differential Structure}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


> infixr 4 <+

> class (Traversable f, Traversable f') => Differentiable f f' | f -> f' where
>   (<+) :: f' x -> x -> f x
>   down :: f x -> f (f' x, x)

> instance Differentiable (Const k) (Const Zero) where
>   Const z <+ x = naughty z
>   down (Const k) = Const k

> instance Differentiable Id (Const ()) where
>   _ <+ x = Id x
>   down (Id x) = Id (Const (), x)

> instance (Differentiable p p', Differentiable q q') =>
>   Differentiable (Sum p q) (Sum p' q') where
>   Inl  p' <+ x  = Inl  (p' <+ x)
>   Inr  q' <+ x  = Inr  (q' <+ x)
>   down (Inl  p) = Inl   $ fmap (\ (p', x) -> (Inl p', x)) (down p)
>   down (Inr  q) = Inr   $ fmap (\ (q', x) -> (Inr q', x)) (down q)

> instance (Differentiable p p', Differentiable q q') =>
>   Differentiable (Prod p q) (Sum (Prod p' q) (Prod p q')) where
>   Inl  (p' :*: q) <+ x = (p' <+ x) :*: q
>   Inr  (p :*: q') <+ x = p :*: (q' <+ x)
>   down (p :*: q)
>     =    fmap (\ (p', x) -> (Inl (p' :*: q), x)) (down p)
>     :*:  fmap (\ (q', x) -> (Inr (p :*: q'), x)) (down q)

> instance (Differentiable p p', Differentiable q q') =>
>   Differentiable (Compo p q) (Prod (Compo p' q) q') where
>   (Comp p'q :*: q') <+ x = Comp (p'q <+ q' <+ x)
>   down (Comp pq) = Comp $
>     fmap (\ (p'q, q) ->
>       fmap (\ (q', x) ->
>         (Comp p'q :*: q', x)
>       ) (down q)
>     ) (down pq)



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Monadic Case Analysis}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

I'm fed up writing

< do  b <- mb
<     if b
<       then mt
<       else me

and its case analysis friends.

Hence this thing:

> class Case d a | d -> a, a -> d where
>   casey :: a t -> d -> t
>   (?) :: Monad m => m d -> a (m t) -> m t
>   md ? alg = md >>= casey alg

> data BoolCase t = BoolCase {
>   true :: t,
>   false :: t}

> instance Case Bool BoolCase where
>   casey alg True   = true alg
>   casey alg False  = false alg

So now we write

< mb ? BoolCase {
<   true = mt,
<   false = me}

which nests better. It's still annoying.

> data MaybeCase a t = MaybeCase {
>   just :: a -> t,
>   nothing :: t}

> instance Case (Maybe a) (MaybeCase a) where
>   casey alg (Just a)  = just alg a
>   casey alg Nothing   = nothing alg

> data EitherCase a b t = EitherCase {
>   left   :: a -> t,
>   right  :: b -> t}

> instance Case (Either a b) (EitherCase a b) where
>   casey alg (Left a)   = left alg a
>   casey alg (Right b)  = right alg b


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Constructing Monads}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

I introduce a very general monad transformer, adding fixed inputs,
mutable state, accumlating outputs and exceptions.


> newtype Mo ls i s o e m x = Mach (i -> s -> m (Either e (x, s, o)))

> instance Unpack (Mo ls i s o e m x) (i -> s -> m (Either e (x, s, o))) where
>   un (Mach f) = f

The |ls| parameter is a phantom parameter for the \emph{labels} which
I'll use to control the \emph{syntax} of computations. The other
parameters give the semantics.  Instantiating them with the
appropriate neutral elements gives us a trivial transformation which
we can always undo.

> type Base = Mo () () () () Zero

> mach :: Monad m => Base m x -> m x
> mach (Mach f) = f () () ? EitherCase {
>   left = naughty,
>   right = \ (x, _, _) -> return x}

> purely :: Base Id t -> t
> purely = op Id . mach


Provided the output is a |Monoid| and the underlying |m| is a |Monad|,
our transformed thing is also a |Monad|, hence lots of other stuff too.
Here, we get to see how these machines work.

> instance (Monad m, Monoid o) => Monad (Mo ls i s o e m) where
>   return x = Mach $ \_ s -> return (Right (x, s, zero))
>   Mach g >>= f = Mach $ \i s -> g i s ? EitherCase {
>     left   = return . Left,
>     right  = \ (x, s, o) -> op Mach (f x) i s ? EitherCase {
>       left   = \ e -> return (Left e),
>       right  = \ (y, s, p) ->
>         return (Right (y, s, o <+> p)) }}

> instance (Monad m, Monoid o) => Applicative (Mo ls i s o e m) where
>   pure = return
>   (<*>) = ap

> instance (Monad m, Monoid o) => Functor (Mo ls i s o e m) where
>   fmap = (<*>) . pure

The idea here is that instead of piling monad transformers on top of |m|,
we adjust the parameters individually. First let's show how to work with the
semantics. We need to show how each new capability works, and how the old
capabilities are preserved.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Lifting and Acting}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\paragraph{Adding a fixed input.} Extending the |i| component gives us a new
\emph{read} action.

> readAct :: (Monad m, Monoid o) => Mo ls (i, r) s o e m r
> readAct = Mach $ \ (i, r) s -> return (Right (r, s, zero))

But we can certainly lift all the old functionality.

> readLift :: Mo ls i s o e m x -> Mo ls (i, r) s o e m x
> readLift (Mach f) = Mach $ \ (i, r) s -> f i s


\paragraph{Extending the state.} This gives us \emph{get} and \emph{put}
functionality.

> getAct :: (Monad m, Monoid o) => Mo ls i (s, u) o e m u
> getAct = Mach $ \i su@(_, u) -> return (Right (u, su, zero))

> putAct :: (Monad m, Monoid o) => u -> Mo ls i (s, u) o e m ()
> putAct u = Mach $ \i (s, _) -> return (Right ((), (s, u), zero))

> stateLift :: (Monad m) => Mo ls i s o e m x -> Mo ls i (s, u) o e m x
> stateLift (Mach f) = Mach $ \i (s, u) -> f i s ? EitherCase {
>   left   = return . Left,
>   right  = \ (x, s, o) -> return (Right (x, (s, u), o)) }


\paragraph{Adding a writer.} Extending the |o| monoid with another field
gives us a new \emph{write} action.

> writeAct :: (Monad m, Monoid o, Monoid p) => p -> Mo ls i s (o, p) e m ()
> writeAct p = Mach $ \ i s -> return (Right ((), s, (zero, p)))

> writeLift :: (Monad m, Monoid p) =>
>   Mo ls i s o e m x -> Mo ls i s (o, p) e m x
> writeLift (Mach f) = Mach $ \i r -> f i r ? EitherCase {
>   left   = return . Left,
>   right  = \ (x, s, o) -> return (Right (x, s, (o, zero))) }


\paragraph{Adding a new exception.} This gives us a \emph{throw} action.

> throwAct :: Monad m => d -> Mo ls i s o (Either e d) m x
> throwAct d = Mach $ \_ _ -> return (Left (Right d))

> exnLift :: Monad m => Mo ls i s o e m x -> Mo ls i s o (Either e d) m x
> exnLift (Mach f) = Mach $ \i s -> f i s ? EitherCase {
>   left = return . Left . Left,
>   right = return . Right}

\paragraph{Changing the labels.} This has no semantic consequences.

> labelLift :: Mo ls i s o e m x -> Mo (l ls) i s o e m x
> labelLift (Mach f) = Mach f


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Labelling Actions}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Here I abstract over the capabilities which a notion of computation
can offer, by explaining how each |m| maps a label |l| to a
computation parametrised by an |s|, returning a value in |t|.

> class Action m l s t | m l s -> t, m l t -> s where
>   act :: l -> s -> m t

Anything |m| can do, |Base m| can also do, as they are isomorphic.

> instance (Applicative m, Action m l s t) => Action (Base m) l s t where
>   act l s = Mach $ \_ _ -> iI basic (act l s) Ii where
>     basic x = Right (x, (), ())

Now, for each new kind of functionality, we create suitable labels to describe
the actions, then show how to wire the labels to the semantics.

\paragraph{Reader.} Each new reader offers two new actions and preserves the
old ones.

> data ReadLabel l r ls = ReadLabel l ls

> data Rd l = Rd l

> instance (Monad m, Monoid o) =>
>   Action (Mo (ReadLabel l r ls) (i, r) s o e m) (Rd l) () r where
>   act _ () = readAct

All other actions get lifted through the new reader.

> instance (Monad m, Monoid o, Action (Mo ls i s o e m) k a b) =>
>   Action (Mo (ReadLabel l r ls) (i, r) s o e m) k a b where
>   act k a = labelLift $ readLift $ act k a

Now I add a handy user interface, largely intended to alleviate
parenthesis overload.


> (?=) :: l -> r  -> Mo (ReadLabel l r ls) (i, r) s o e m x
>                 -> Mo ls i s o e m x
> (l ?= r) (Mach f) = Mach $ \i s -> f (i, r) s

> rd :: Action m (Rd l) () r => l -> m r
> rd l = act (Rd l) ()

For example, given handy types

> data ExA = ExA
> data ExB = ExB

< purely $ ExA ?= True $ ExB ?= 'c' $ rd ExA == True
< purely $ ExA ?= True $ ExB ?= 'c' $ ExA ?= 3 $ rd ExA == 3

with shadowing!

\paragraph{State.} The top level interface to state has a read action as
above, but adds a write action.

> data StateLabel l u ls = StateLabel l ls

> data Wr l = Wr l

> instance (Monad m, Monoid o) =>
>   Action (Mo (StateLabel l u ls) i (s, u) o e m) (Rd l) () u where
>   act _ () = getAct

> instance (Monad m, Monoid o) =>
>   Action (Mo (StateLabel l u ls) i (s, u) o e m) (Wr l) u () where
>   act _ t = putAct t

> instance (Monad m, Monoid o, Action (Mo ls i s o e m) k a b) =>
>   Action (Mo (StateLabel l u ls) i (s, u) o e m) k a b where
>   act k a = labelLift $ stateLift $ act k a

We already have the |rd| interface for the `get' action. Here's the
assignment\ldots


> (\=) :: Action m (Wr l) u () => l -> u -> m ()
> l \= u = act (Wr l) u

> modify ::  (  Applicative m, Monad m,
>               Action m (Rd l) () u, Action m (Wr l) u ()) =>
>            l -> (u -> u) -> m ()
> modify l f = iI (l \=) (f <$> rd l) Ji

\ldots{}and here's how to create new state.

> (!=) :: (Monad m, Monoid o) =>
>   l -> u -> Mo (StateLabel l u ls) i (s, u) o e m x -> Mo ls i s o e m x
> (l != u) (Mach f) = Mach $ \i s -> f i (s, u) ? EitherCase {
>   left = return . Left,
>   right = \ (x, (s, _), o) -> return (Right (x, s, o))}


\paragraph{Writing.} Writers just have a write action, returning a value
in the selected component of the output.

> data WriteLabel l p ls = WriteLabel l ls

> instance (Monad m, Monoid o, Monoid p) =>
>   Action (Mo (WriteLabel l p ls) i s (o, p) e m) (Wr l) p () where
>     act _ p = writeAct p

> instance (Monad m, Monoid p, Action (Mo ls i s o e m) k a b) =>
>   Action (Mo (WriteLabel l u ls) i s (o, p) e m) k a b where
>   act k a = labelLift $ writeLift $ act k a

To introduce a new writer, we can just ask to compute a value in a monoid.

> accum :: (Monad m, Monoid p) =>
>   l -> Mo (WriteLabel l p ls) i s (o, p) e m () -> Mo ls i s o e m p
> accum l (Mach f) = Mach $ \i r -> f i r ? EitherCase {
>   left = return . Left,
>   right = \ (_, s, (o, p)) -> return (Right (p, s ,o)) }

Or we can ask to do so, in addition to other work.

> alsoAccum :: (Monad m, Monoid p) =>
>   l -> Mo (WriteLabel l p ls) i s (o, p) e m x -> Mo ls i s o e m (x, p)
> alsoAccum l (Mach f) = Mach $ \i r -> f i r ? EitherCase {
>   left = return . Left,
>   right = \ (x, s, (o, p)) -> return (Right ((x, p), s ,o)) }



\paragraph{Exceptions.} A new `throw' capability is local to a |catch|.

> data ExnLabel l d ls = ExnLabel l ls

> data Thr l = Thr l

> instance Monad m =>
>   Action (Mo (ExnLabel l d ls) i s o (Either e d) m) (Thr l) d Zero where
>   act _ d = throwAct d

> instance (Monad m, Monoid o, Action (Mo ls i s o e m) k a b) =>
>   Action (Mo (ExnLabel l d ls) i s o (Either e d) m) k a b where
>   act k a = labelLift $ exnLift $ act k a

> (\|/) :: (Applicative m, Action m (Thr l) e Zero) => l -> e -> m a
> l \|/ e = naughty <$> act (Thr l) e

> catch ::  (Monad m, Monoid o) =>
>           l -> Mo (ExnLabel l d ls) i s o (Either e d) m x ->
>           (d -> Mo ls i s o e m x) -> Mo ls i s o e m x
> catch l c h = Mach $ \i s -> op Mach c i s ? EitherCase {
>   left = \ed -> case ed of
>     Left e -> return (Left e)
>     Right d -> op Mach (h d) i s, -- exception restores initial state
>   right = return . Right}

^ ^ ^ ^ ^ ^ ^

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Pushing}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

For a typical reader, one should be able to modify the environment
locally. That requires a bit of extra chewing gum.

> data Proxy a = Proxy

> class MoLocally ls l r i | ls l -> r i  where
>   moLocally :: Proxy ls -> l -> (r -> r) -> (i -> i)

> instance MoLocally (ReadLabel l r ls) l r (i, r) where
>   moLocally _ _ p (i, r) = (i, p r)

> instance MoLocally ls l r i => MoLocally (ReadLabel k s ls) l r (i, s) where
>   moLocally _ l p (i, s) = (moLocally (Proxy :: Proxy ls) l p i, s)

> instance MoLocally ls l r i => MoLocally (k ls) l r i where
>   moLocally _ = moLocally (Proxy :: Proxy ls)

> class Locally m l r | m l -> r where
>   locally :: (r -> r) -> l -> m t -> m t

> instance MoLocally ls l r i => Locally (Mo ls i s o e m) l r where
>   locally p l (Mach f :: Mo ls i s o e m t) =
>     Mach (f . moLocally (Proxy :: Proxy ls) l p)

> (?/) :: Locally m l r => l -> r -> m t -> m t
> l ?/ r = locally (const r) l

In particular, we can |locally| change a reader without
losing any of the monad's other functionality. Some examples, showing what
happens.

< purely $ ExA ?= True $ ExB ?= 'c' $ locally not ExA $ rd ExA
<   == False

< purely $ ExA ?= True $ ExB ?= 'c' $ locally not ExA $ rd ExB
<   == 'c'

< purely $ ExA ?= True $ ExB ?= 'c' $
<   iI (,) (locally not ExA $ rd ExA) (rd ExA) Ii == (False, True)

Just a wee experiment.

> reverseWords :: String -> String
> reverseWords s = purely $ ExA != "" $ ExB != "" $ do
>   for s $ \c -> if c == ' '
>     then iI (modify ExB) (moo <$> rd ExA) Ji >> (ExA \= zero)
>     else modify ExA (c :)
>   iI moo (rd ExA) (rd ExB) Ii
>   where
>     moo "" s = s
>     moo w "" = gloo w ""
>     moo w  s = gloo w (' ' : s)
>     gloo xs ys = foldl (flip (:)) ys xs

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\section{Detritus}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Either}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% instance Monad (Either x) where
%   return          = Right
%   Left x   >>= _  = Left x
%   Right s  >>= f  = f s

% instance Applicative (Either x) where
%   pure   = return
%   (<*>)  = ap

% instance Monoid x => Monoid (Either x t) where
%   mempty  = Left zero
%   mappend (Right t)  _          = Right t
%   mappend (Left _)   (Right t)  = Right t
%   mappend (Left x)   (Left y)   = Left (x <+> y)

% raise :: x -> Either x t
% raise = Left

% handle :: Either x t -> (x -> Either x t) -> Either x t
% handle (Left x) f = f x
% handle rt       _ = rt

% eitherMapL :: (a -> b) -> Either a c -> Either b c
% eitherMapL f = either (Left . f) Right


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Rather}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% data Rather x = Rats | Rather x deriving (Show,Eq)

% instance Monoid (Rather x) where
%   mempty = Rats
%   x `mappend` Rats = x
%   _ `mappend` y    = y

% instance Monad Rather where
%   return = Rather
%   Rats >>= _ = Rats 
%   Rather x >>= f = f x 

% instance Applicative Rather where
%   pure = return
%   (<*>) = ap


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{State}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% instance Applicative (State s) where
%   pure   = return
%   (<*>)  = ap

% instance Monoid x => Monoid (State s x) where
%   mempty         = iI zero Ii
%   mappend sx sy  = iI (<+>) sx sy Ii

% instance Monad m => Applicative (StateT s m) where
%   pure   = return
%   (<*>)  = ap

% instance (Monad m, Monoid x) => Monoid (StateT s m x) where
%   mempty         = iI zero Ii
%   mappend sx sy  = iI (<+>) sx sy Ii


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Reader}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% instance Applicative (Reader s) where
%   pure   = return
%   (<*>)  = ap

% instance Monoid x => Monoid (Reader s x) where
%   mempty         = iI zero Ii
%   mappend sx sy  = iI (<+>) sx sy Ii

% instance Monad m => Applicative (ReaderT s m) where
%   pure   = return
%   (<*>)  = ap

% instance (Monad m, Monoid x) => Monoid (ReaderT s m x) where
%   mempty         = iI zero Ii
%   mappend sx sy  = iI (<+>) sx sy Ii


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{IO}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% instance Monoid x => Monoid (IO x) where
%   mempty         = iI zero Ii
%   mappend sx sy  = iI (<+>) sx sy Ii



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\subsection{Threading Environments}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% class Applicative i => Environmental i k | i -> k where
%   given  :: (k -> i x) -> i x
%   for    :: k -> i x -> i x
%   push   :: (k -> k) -> i x -> i x
%   push f ix = given $ \t -> for (f t) ix

% instance Environmental ((->) r) r where
%   given  f r  = f r r
%   for    r f  = pure (f r)


% instance  (Environmental i k, Applicative j) =>
%           Environmental (Comp i j) k where
%   given  f  = Comp (given (op Comp . f))
%   for    k  = Comp . for k . op Comp

% instance Environmental (State x) x where
%   given f = f =<< get
%   for temp c = do
%     old <- get
%     put temp
%     v <- c
%     put old
%     return v

% instance Monad m => Environmental (StateT x m) x where
%   given f = f =<< get
%   for temp c = do
%     old <- get
%     put temp
%     v <- c
%     put old
%     return v





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Monadic control operators
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% miffy :: Monad m => m Bool -> m t -> m t -> m t
% miffy mb mt me = do
%   b <- mb
%   if b then mt else me

% mmaybe :: Monad m => m (Maybe x) -> m t -> (x -> m t) -> m t
% mmaybe mmx mn mj = do
%   mx <- mmx
%   case mx of
%     Nothing  -> mn
%     Just x   -> mj x

% meither :: Monad m => m (Either l r) -> (l -> m t) -> (r -> m t) -> m t
% meither me ml mr = do
%   e <- me
%   case e of
%     Left l   -> ml l
%     Right r  -> mr r

% infixl 0 %
% (%) = ($)

% instance Monoid a => Applicative ((,) a) where
%   pure x = (zero,x)
%   (a,f) <*> (b,x) = (a <+> b,f x)

\bibliographystyle{named}
\bibliography{EpiTome}




\end{document}