%ghci -Wall Holes.lhs

%if False

> {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
> module Holes where

> import Control.Monad
> import Control.Applicative
> import Control.Arrow((***))
> import Data.Foldable
> import Data.Traversable
> import Data.Monoid hiding (Sum)
> import GHC.Prim

%endif

\documentclass{jfp}
\usepackage{stmaryrd,wasysym,url,upgreek}

%include lhs2TeX.fmt
%include lhs2TeX.sty
%include jfpcompat.sty
%include polycode.fmt
\DeclareMathAlphabet{\mathkw}{OT1}{cmss}{bx}{n}

\newcommand{\FN}{\mathsf}

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

\newcommand{\comment}[1]{\marginpar{#1}}

\newenvironment{axioms}
	{\par\vspace{\abovedisplayskip}\noindent\begin{tabular}{@@{}lrcl@@{}}}
	{\end{tabular}\vspace{\belowdisplayskip}\par\ignorespaces\noindent}
\newcommand{\axiomname}[1]{\textbf{\textsf{#1}}}

\newcommand{\LLabel}[1]{\vcenter{\llap{#1}}}
\newcommand{\RLabel}[1]{\vcenter{\rlap{#1}}}

\begin{document}

\title{Why walk when you can take the tube?}
\author[Lucas Dixon, Peter Hancock and Conor McBride]
       {LUCAS DIXON\\
        University of Edinburgh
        \and PETER HANCOCK and CONOR MCBRIDE\\
        University of Nottingham}
\maketitle[F]

\begin{abstract}
Mornington Crescent
\end{abstract}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%format id = "\FN{id}"
%format . = "\cdot"
%format <*> = "\circledast "
%format <$> = "\mathop{<\!\!\!\$\!\!\!>}"
%format pure = "\FN{pure}"
%format traverse = "\FN{traverse}"
%format uncurry = "\FN{uncurry}"
%format fmap = "\FN{fmap}"
%format ap = "\FN{ap}"
%format return = "\FN{return}"
%format snd = "\FN{snd}"
%format *** = "\times "
%format mappend (x) (y) = x "\oplus" y
%format mempty = "\varepsilon"
%format fst = "\FN{fst}"

%if False

> instance Monoid (Maybe x) where
>   mempty = Nothing
>   mappend Nothing  y = y
>   mappend x        _ = x

%endif
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}
\label{sec:introduction}

The purpose of this paper is not only
self-citation~\cite{conor:derivative,
conor.ross:applicative.functors}, but also to write a nice wee program.


\section{Traversable Polynomial Functors}
\label{sec:polynomials}

We're going to work generically with recursive datatypes representing
terms in some syntax. The syntax will be determined by a functor |f ::
* -> *|, representing the choice of expression forms.  The parameter
is used to indicate the places for subterms within terms, and the
resulting type of terms is given by taking the least fixpoint of |f|,
so that the parameter gets instantiated with the very type of terms we are
defining.

%format Mu = "\upmu"
%format phi = "\phi"
%format cata = "\FN{cata}"
%format eval = "\FN{eval}"

> newtype Mu f = In (f (Mu f))

To work with data in this style, we'll need a kit for building functors.
Let's start with the \emph{polynomials}, given as follows---in each definition,
|x| represents the type of subterms:

%format Sum (p) (q) = p "\mathop{\:\boxplus\:}" q
%format Prod (p) (q) = p "\boxtimes" q
%format :*: = "\boxtimes"

> newtype  Id          x = Id x  -- `identity' for a subterm
> newtype  C c         x = C c   -- `constant' for non-recursive data of type |c|
> data     (Sum p q)   x = InL (p x) | InR (q x)  -- `sum' for choice
> data     (Prod p q)  x = p x :*: q x            -- `product' for pairing

For a simple example, consider the syntax of expressions with numeric
constants and addition, directly defined thus:

< data Expr = Num Int | Add Expr Expr

We can build this from our kit by describing the basic choice of expression
forms---a non-recursive |Int| or pair of subterms:

> type ExprF = Sum (C Int) (Prod Id Id)

Now, the resulting fixpoint, |Mu ExprF|, is isomorphic to |Expr|, and
we can define the analogues of |Expr|'s constructors.

%format mnum = "\FN{num}"
%format madd = "\FN{add}"
%format e1 = "e_1"
%format e2 = "e_2"

> mnum :: Int -> Mu ExprF
> mnum i = In (InL (C i))
>
> madd :: Mu ExprF -> Mu ExprF -> Mu ExprF
> madd e1 e2 = In (InR (Id e1 :*: Id e2))

This method of constructing datatypes as fixpoints of functors is
entirely standard: a comprehensive account can be found in Bird and de
Moor's \emph{Algebra of Programming}~\cite{bird.demoor:algebra}.  The
point of casting datatypes in this uniform mould is to capture
\emph{patterns} of operations over a class of datatypes, once and for all.
Paradigmatically, for each functor |f|, |Mu f| has an iteration
operator, or \emph{catamorphism}, which explains how to compute
recursively over whole terms, by applying at each node an \emph{algebra}
|phi| to compute the output for a term, given the outputs from its subterms.

> cata :: Functor f => (f t -> t) -> Mu f -> t
> cata phi (In fm) = phi (fmap (cata phi) fm)

For example, we can write an evaluator as a catamorphism whose algebra
explains how each of the expression forms operates on \emph{values}:

%format v1 = "v_1"
%format v2 = "v_2"

> eval :: Mu ExprF -> Int
> eval = cata phi where
>   phi :: ExprF Int -> Int
>   phi (In (InL (C i)))              = i
>   phi (In (InR (Id v1 :*: Id v2)))  = v1 + v2

Of course, we must show that the polynomial type constructors are indeed
functorial. We do this by writing four instances of the |Functor|
class, showing that |Id| and |C c| \emph{are} functors, whilst |Sum|
and |Prod| \emph{preserve} functoriality. Recall that a |Functor|
in Haskell is just a type constructor |f| which supports the overloaded
`map'  operation, |fmap :: (s -> t) -> f s -> f t|.

> instance Functor Id where
>   fmap f (Id x) = Id (f x)
>
> instance Functor (C c) where
>   fmap f (C c) = (C c)
>
> 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 (Functor p, Functor q) => Functor (Prod p q) where
>   fmap f (px :*: qx) = fmap f px :*: fmap f qx

But we can have more than that! In~\cite{conor.ross:applicative.functors},
McBride and Paterson introduced the notion of a |Traversable| functor,
delivering a version of `map' which performs an \emph{effectful}
computation for each element, combining the effects:

< class Functor f => Traversable f where
<   traverse :: Applicative a => (s -> a t) -> f s -> a (f t)

Recall that an |Applicative| functor has the following operations (hence any
|Monad| can be made |Applicative|):

< class Functor a => Applicative a where
<   pure   :: x -> a x                   -- values become effectless |a|-computations
<   (<*>)  :: a (s -> t) -> a s -> a t   -- |a|-application, combining effects

Implementing |traverse| is just like implementing |fmap|, except that
we use |pure| to lift the constructors and we replace
the ordinary application with |a|-application. We think of working in this
lifted way as `programming in the \emph{idiom} of |a|'.

> instance Traversable Id where
>   traverse f (Id x) = pure Id <*> f x
>
> instance Traversable (C c) where
>   traverse f (C c) = pure (C c)
>
> instance (Traversable p, Traversable q) => Traversable (Sum p q) where
>   traverse f (InL px)  = pure InL  <*> traverse f px
>   traverse f (InR qx)  = pure InR  <*> traverse f qx
>
> instance (Traversable p, Traversable q) => Traversable (Prod p q) where
>   traverse f (px :*: qx) = pure (:*:) <*> traverse f px <*> traverse f qx

We shall be making particular use of traversability in the |Maybe|
idiom, lifting a \emph{failure-prone} function |f| on elements to a
traversal which succeeds only if |f| succeeds at every element.

[|lookup| example.]
[|traverse| with |Maybe| is strict, so doesn't work on streams.]

\textbf{Remark.} Every |Traversable| functor must be an instance of
|Functor|. We can easily implement |fmap| by using |traverse| with |a
= Id|.

[You don't get closure under functoriality from closure under traversability.]
[A pair of streams is still functorial.]


\subsection{Composition}

%format Dot (p) (q) = p "\boxcircle" q

> newtype (Dot p q) x = Comp (p (q x))
>
> instance (Traversable p, Traversable q) => Traversable (Dot p q) where
>   traverse f (Comp xqp) = pure Comp <*> traverse (traverse f) xqp

%if False

> instance Foldable Id where
>   foldMap f (Id x) = f x


> instance Foldable (C c) where
>   foldMap f _ = mempty

> instance (Foldable p, Foldable q) => Foldable (Sum p q) where
>   foldMap f (InL ps) = foldMap f ps
>   foldMap f (InR qs) = foldMap f qs


> instance (Foldable p, Foldable q) => Foldable (Prod p q) where
>   foldMap f (ps :*: qs) = foldMap f ps `mappend` foldMap f qs


> instance (Foldable p, Foldable q) => Foldable (Dot p q) where
>   foldMap f (Comp xpq) = foldMap (foldMap f) xpq

> instance (Functor p, Functor q) => Functor (Dot p q) where
>   fmap f (Comp xpq) = Comp (fmap (fmap f) xpq)

%endif

\section{Free Monads}

The \emph{free monad} construction lifts any functorial
\emph{signature} |p| of operations to a \emph{syntax} of expressions
constructed from those operations and from free variables |x|.

> data Term p x = Con (p (Term p x)) | Var x

The |return| of the |Monad| embeds free variables into the syntax. The |>>=|
is exactly the simultaneous substitution operator. Below, |f| takes variables
in |x| to expressions in |Term p y|; |(>>= f)| delivers the corresponding
action on expressions in |Term p x|.

> instance Functor p => Monad (Term p) where
>   return = Var
>   Var x   >>= f = f x
>   Con tp  >>= f = Con (fmap (>>= f) tp)

Correspondingly, |Term p| is also |Applicative| and a |Functor|. Moreover,
if |p| is |Traversable|, then so is |Term p|.

%if False

> instance Functor p => Applicative (Term p) where
>   pure = return
>   (<*>) = ap

> instance Functor p => Functor (Term p) where
>   fmap = (<$>)

> instance Foldable p => Foldable (Term p) where
>   foldMap f (Var x)   = f x
>   foldMap f (Con tp)  = foldMap (foldMap f) tp

%endif

> instance Traversable p => Traversable (Term p) where
>   traverse f (Var x)   = pure Var <*> f x
>   traverse f (Con tp)  = pure Con <*> traverse (traverse f) tp

By way of example, we choose a simple signature with constant integer values
and a binary operator\footnote{Hutton's Razor strikes again!}. As one might
expect, |Sum| delivers choice and |Prod| delivers pairing. Meanwhile |Id|
marks the spot for each subexpression.

> type Sig = Sum (C Int) (Prod Id Id)

Now we can implement the constructors we first thought of, just by plugging
|Con| together with the constructors of the polynommial functors in |Sig|.

[Relate this to the direct presentation of expressions.]

%format val = "\FN{val}"

> val :: Int -> Term Sig x
> val i = Con (InL (C i))

%format add = "\FN{add}"

> add :: Term Sig x -> Term Sig x ->  Term Sig x
> add x y = Con (InR (Id x :*: Id y))


%format Zero = "\emptyset"

\section{The |Zero| Type}

We can recover the idea of a \emph{closed} term by introducing the
|Zero| type, beloved of logicians but sadly too often spurned by programmers.

> data Zero

Bona fide elements of |Zero| are hard to come by, so we may safely offer to
exchange them for anything you might care to want: as you will be paying with
bogus currency, you cannot object to our shoddy merchandise.

%format naughtE = "\FN{naughtE}"

> naughtE :: Zero -> a
> naughtE _ = undefined

More crucially, |naughtE| lifts functorially. The type |f Zero| represents
the `base cases' of |f| which exist uniformly regardless of |f|'s argument.
For example, |[] :: [Zero]|, |Nothing :: Maybe Zero| and |C 3 :: Sig Zero|.
We can map these terms into any |f a|, just by turning all the elements of
|Zero| we encounter into elements of |a|.

%format inflate = "\FN{inflate}"

> inflate :: Functor f => f Zero -> f a
> inflate = unsafeCoerce# -- |fmap naughtE|  -- could be |unsafeCoerce|

Thus equipped, we may take |Term p Zero|
to give us the \emph{closed} terms over signature |p|. Modulo the
usual fuss about bottoms, |Term p Zero| is
just the usual recursive datatype given by taking the fixpoint of |p|.
The general purpose
`evaluator' for closed terms is just the usual notion of \emph{catamorphism}.

%format fcata = "\FN{fcata}"

> fcata :: (Functor p) => (p v -> v) -> Term p Zero -> v
> fcata operate (Var nonsense)    = naughtE nonsense
> fcata operate (Con expression)  = operate (fmap (fcata operate) expression)

Following our running example, we may take

%format sigOps = "\FN{sigOps}"

> sigOps :: Sig Int -> Int
> sigOps (InL (C i))          = i
> sigOps (InR (Id x :*: Id y))  = x + y

and now

< cata sigOps (add (val 2) (val 2)) = 4

We shall also make considerable use of |Zero| in a moment, when we start making
\emph{holes} in polynomials.


\section{Differentiating Polynomials}
\label{sec:differentiating}

[Need the usual pictures, and some examples.]

%if False

> infixr 4 <.

%endif

%format <. = "\mathop{<\!\!\!\cdot}"

%format const = "\FN{const}"
%format down = "\FN{down}"
%format Diff p (d) = "\partial" p "\mapsto" d

> class (Traversable p, Traversable p') => Diff p p' | p -> p' where
>   (<.) :: p' x -> x -> p x
>   down :: p x -> p (p' x, x)

\begin{axioms}
\axiomname{downright}
   & |fmap snd (down xf)| & = & |xf| \\
\axiomname{downhome}
   & |fmap (uncurry (<.)) (down xf)| & = & |fmap (const xf) xf| \\
\end{axioms}

> instance Diff (C c) (C Zero) where
>   C z <. _ = naughtE z
>   down (C c) = C c

> instance Diff Id (C ()) where
>   C () <. x = Id x
>   down (Id x) = Id (C (), x)

> instance (Diff p p', Diff q q') => Diff (Sum p q) (Sum p' q') where
>   InL p' <. x = InL (p' <. x)
>   InR q' <. x = InR (q' <. x)
>   down (InL p) = InL (fmap (InL *** id) (down p))
>   down (InR q) = InR (fmap (InR *** id) (down q))

> instance (Diff p p', Diff q q') => Diff (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 ((InL . (:*: q)) *** id) (down p) :*: fmap ((InR . (p :*:)) *** id) (down q)

%format outer = "\FN{outer}"
%format inner = "\FN{inner}"

> instance (Diff p p', Diff q q') => Diff (Dot p q) (Prod ((Dot p' q)) q') where
>   (Comp p' :*: q') <. x = Comp (p' <. q' <. x)
>   down (Comp xqp) = Comp (fmap outer (down xqp)) where
>     outer (p', xq) = fmap inner (down xq) where
>       inner (q', x) = (Comp p' :*: q', x)


\section{Differentiating Free Monads}

A one-hole context in the syntax of |Term|s generated by the free monad
construction is just a \emph{sequence} of one-hole contexts for subterms in
terms, as given by differentiating the signature functor.

> newtype Diff p p' => Tube p p' x = Tube [p' (Term p x)]

|Tube|s are |Traversable| |Functor|s. They also inherit a
|Monoid| structure from their underlying representation of
sequences. Exactly which sequence structure you should use depends on
the operations you need to support. As in~\cite{conor:derivative}, we
are just using good old |[]| for pedagogical simplicity. At the time,
Ralf Hinze, Johan Jeuring and Andres L\"oh pointed
out~\shortcite{hinze.jeuring.loh:tidts}, this choice does not yield
constant-time \emph{navigation} operations in the style of Huet's
`zippers'~\shortcite{huet:zipper}, and I am sure they would not
forgive us this time if we failed to mention that replacing |[]| by
`snoc-lists' which grow on the right restores this facility.

Let us give an interface to contexts. We shall need the |Monoid| structure:

> instance Diff p p' => Monoid (Tube p p' x) where
>   mempty = Tube []
>   mappend  ctxt       (Tube [])   = ctxt
>   mappend  (Tube ds)  (Tube ds')  = Tube (ds ++ ds')

We may construct a one-step context for |Term p| from a one-hole
context for subterms in a |p|.

%format step = "\FN{step}"

> step :: Diff p p' => p' (Term p x) -> Tube p p' x
> step d = Tube [d]

%if False

We can decompose contexts into steps, starting from their `root' end.

%format context = "\FN{context}"

> context :: Diff p p' => Tube p p' x -> t -> (p' (Term p x) -> Tube p p' x -> t) -> t
> context (Tube [])              n c = n
> context (Tube (p'tx : lp'tx))  n c = c p'tx (Tube lp'tx)

%endif

%if False

> instance Diff p p' => Traversable (Tube p p') where
>   traverse f (Tube xtds) = pure Tube <*> traverse (traverse (traverse f)) xtds

> instance Diff p p' => Functor (Tube p p') where
>   fmap = fmapDefault

> instance Diff p p' => Foldable (Tube p p') where
>   foldMap = foldMapDefault

%endif

Plugging a |Term| into a |Tube| just iterates |<.| for |p|.

%format <<. = "\mathop{<\!\!\!<\!\!\!\cdot}"

%if False

> infixr 4 <<.

%endif

> (<<.) :: Diff p p' => Tube p p' x -> Term p x -> Term p x
> Tube [] <<. t = t
> Tube (d : ds) <<. t = Con (d <. Tube ds <<. t)

Moreover, anyplace you can plug a subterm is certainly a place you can
plug a variable, and \emph{vice versa}. We shall also have

> instance Diff p p' => Diff (Term p) (Tube p p') where
>   ctxt <. x = ctxt <<. Var x
>   down (Var x)   = Var (mempty, x)
>   down (Con tp)  = Con (fmap outer (down tp)) where
>     outer (p', t) = fmap inner (down t) where
>       inner (ctxt, x) = (mappend (step p') ctxt, x)


\section{Going Underground}

%format :-<: = "\mathop{:\!\!\!-\!\!\!<\!\!\!:}"

%if False

> infixr 4 :-<:

%endif

> data Diff p p' => Underground p p' x
>   =  Ground (Term p Zero)
>   |  Tube p p' Zero :-<: Node p p' x
>
> data Diff p p' => Node p p' x
>   =  Terminus x
>   |  Junction (p (Underground p p' x))

%format var = "\FN{var}"

> var :: Diff p p' => x -> Underground p p' x
> var x = mempty :-<: Terminus x

%format con = "\FN{con}"
%format ground = "\FN{ground}"
%format tubing = "\FN{tubing}"
%format p'sx = "\mathit{p^\prime\!sx}"
%format p't0 = "\mathit{p^\prime\!t0}"

> con :: Diff p p' => p (Underground p p' x) -> Underground p p' x
> con psx = case traverse compressed psx of
>   Just pt0 -> Ground (Con pt0)
>   Nothing -> case foldMap tubing (down psx) of
>     Just sx -> sx
>     Nothing -> mempty :-<: Junction psx
>   where
>     compressed :: Diff p p' => Underground p p' x -> Maybe (Term p Zero)
>     compressed (Ground pt0)  = Just pt0
>     compressed _             = Nothing
>     tubing (p'sx, bone :-<: node) = case traverse compressed p'sx of
>       Just p't0  -> Just (mappend (step p't0) bone :-<: node)
>       Nothing    -> Nothing
>     tubing _ = Nothing

%format underground = "\FN{underground}"

> underground :: Diff p p' => Underground p p' x -> (x -> t) -> (p (Underground p p' x) -> t) -> t
> underground (Ground (Con pt0))                 v c = c (fmap Ground pt0)
> underground (Tube [] :-<: Terminus x)          v c = v x
> underground (Tube [] :-<: Junction psx)        v c = c psx
> underground (Tube (p't0 : tube) :-<: station)  v c =
>   c (fmap Ground p't0 <. (Tube tube :-<: station))

%format termSkel = "\FN{termSkel}"

> tunnel :: Diff p p' => Term p x -> Underground p p' x
> tunnel (Var x)    = var x
> tunnel (Con ptx)  = con (fmap tunnel ptx)

%format skelTerm = "\FN{skelTerm}"

> untunnel :: Diff p p' => Underground p p' x -> Term p x
> untunnel sx = underground sx
>   (\{-|var|-} x    -> Var x)
>   (\{-|con|-} psx  -> Con (fmap untunnel psx))

%format sgm = "\sigma"

%format -< = "\mathop{-\!\!\!<}"
%format tube0 = "\mathit{tube}_0"
%format tube1 = "\mathit{tube}_1"

%if False

> infixr 4 -<

%endif

> (-<) :: Diff p p' => Tube p p' Zero -> Underground p p' x -> Underground p p' x
> tube   -< Ground pt0  = Ground (tube <<. pt0)
> tube0  -< tube1 :-<: node  = mappend tube0 tube1 :-<: node

> instance Diff p p' => Monad (Underground p p') where
>   return = var
>   Ground pt0                >>= sgm = Ground pt0
>   (tube :-<: Junction psx)  >>= sgm = tube -< con (fmap (>>= sgm) psx)
>   (tube :-<: Terminus x)    >>= sgm = tube -< sgm x


%if False

> class PShow f where
>   pshow :: Show x => f x -> String

> instance Show c => PShow (C c) where
>   pshow (C c) = "(C " ++ show c ++ ")"

> instance PShow Id where
>   pshow (Id x) = "(Id " ++ show x ++ ")"

> instance (PShow p, PShow q) => PShow (Sum p q) where
>   pshow (InL x) = "(InL " ++ pshow x ++ ")"
>   pshow (InR x) = "(InR " ++ pshow x ++ ")"

> instance (PShow p, PShow q) => PShow (Prod p q) where
>   pshow (x :*: y) = "(" ++ pshow x ++ " :*: " ++ pshow y ++ ")"

> instance (PShow p, Show x) => Show (Term p x) where
>   show (Var x) = "(Var " ++ show x ++ ")"
>   show (Con tp) = "(Con " ++ pshow tp ++ ")"

> instance Show Zero where
>   show _ = "Gordon Bennett!"

> instance (Diff p p', PShow p, PShow p', Show x) => Show (Underground p p' x) where
>   show (Ground c) = "(Ground " ++ show c ++ ")"
>   show (tube :-<: Junction sp) =
>     "(" ++ show tube ++ " :-<: Junction " ++ pshow sp ++ ")"
>   show (tube :-<: Terminus x) =
>     "(" ++ show tube ++ " :-<: Terminus " ++ show x ++ ")"

> instance (Diff p p', PShow p, PShow  p', Show x) => Show (Tube p p' x) where
>   show (Tube ds) = "(Tube (" ++ lshow ds ++ "))" where
>     lshow [] = "[]"
>     lshow (x : xs) = pshow x ++ " : " ++ lshow xs






%endif



\bibliographystyle{jfp}
\bibliography{Holes}

\end{document}