%ghci -Wall Holes.lhs

%if False

> {-# OPTIONS -fglasgow-exts #-}
> module Holes where

> import Control.Monad
> import GHC.Prim

%endif

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

%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 crush = "\FN{crush}"
%format *** = "\times "
%format mappend (x) (y) = x "\oplus" y
%format mempty = "\varepsilon"
%format fst = "\FN{fst}"

%if False

> infixl 4 <*>
> infixl 4 <$>

> class Functor f => Applicative f where
>   -- | Lift a value.
>   pure :: a -> f a
>
>   -- | Sequential application.
>   (<*>) :: f (a -> b) -> f a -> f b
>
>   -- | Map
>   (<$>) :: (a -> b) -> f a -> f b
>   f <$> af = pure f <*> af 

> class Functor f => Traversable f where
>   traverse :: Applicative i => (s -> i t) -> f s -> i (f t)
>   dist :: Applicative i => f (i x) -> i (f x)
>   dist = traverse id

> instance Applicative X where
>   pure = X
>   X f <*> X s = X (f s)

> instance Functor X where
>   fmap = fmapDefault

> fmapDefault :: Traversable f => (s -> t) -> f s -> f t
> fmapDefault g sf = case (traverse (X . g) sf) of X t -> t

> instance Traversable [] where
>   traverse f [] = pure []
>   traverse f (x : xs) = pure (:) <*> f x <*> traverse f xs

> class Monoid x where
>   mempty :: x
>   mappend :: x -> x -> x

> instance Monoid x => Applicative (C x) where
>   pure _ = C mempty
>   C x <*> C y = C (mappend x y)

> instance Functor (C x) where
>   fmap = fmapDefault

> crush :: (Monoid t, Traversable f) => (s -> t) -> f s -> t
> crush m sf = case (traverse (C . m) sf) of C t -> t

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

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

> (***) :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> (***) f g (a, b) = (f a, g b)

%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{Polynomial Traversable Functors}
\label{sec:polynomials}

> newtype C c x = C c
>
> instance Traversable (C c) where
>   traverse f (C c) = pure (C c)

> newtype X x = X x
>
> instance Traversable X where
>   traverse f (X x) = pure X <*> f x

%format Sum (p) (q) = p "\,\boxplus\," q

> data (Sum p q) x = InL (p x) | InR (q x)
>
> instance (Traversable p, Traversable q) => Traversable (Sum p q) where
>   traverse f (InL xp)  = pure InL  <*> traverse f xp
>   traverse f (InR xq)  = pure InR  <*> traverse f xq

%format Prod (p) (q) = p "\boxtimes" q
%format :*: = "\boxtimes"

> data (Prod p q) x = p x :*: q x
>
> instance (Traversable p, Traversable q) => Traversable (Prod p q) where
>   traverse f (xp :*: xq) = pure (:*:) <*> traverse f xp <*> traverse f xq

%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 (Functor p, Functor q) => Functor (Sum p q) where
>   fmap f (InL xp) = InL (fmap f xp)
>   fmap f (InR xq) = InR (fmap f xq)

> instance (Functor p, Functor q) => Functor (Prod p q) where
>   fmap f (xp :*: xq) = fmap f xp :*: fmap f xq

> 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 = (<$>)

%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 |X|
marks the spot for each subexpression.

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

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

%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 (X x :*: X 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 cata = "\FN{cata}"

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

Following our running example, we may take

%format sigOps = "\FN{sigOps}"

> sigOps :: Sig Int -> Int
> sigOps (InL (C i))          = i
> sigOps (InR (X x :*: X 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}

%if False

> infixr 4 <.

%endif

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

%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 X (C ()) where
>   C () <. x = X x
>   down (X x) = X (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 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 :: 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


%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 crush 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 X where
>   pshow (X x) = "(X " ++ 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 (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}