+\subsubsection{Naming and substituting}
+
+Perhaps surprisingly, one of the most fundamental challenges in
+implementing a theory of the kind presented is choosing a good data type
+for terms, and specifically handling substitutions in a sane way.
+
+There are two broad schools of thought when it comes to naming
+variables, and thus substituting:
+\begin{description}
+\item[Nameful] Bound variables are represented by some enumerable data
+ type, just as we have described up to now, starting from Section
+ \ref{sec:untyped}. The problem is that avoiding name capturing is a
+ nightmare, both in the sense that it is not performant---given that we
+ need to rename rename substitute each time we `enter' a binder---but
+ most importantly given the fact that in even more slightly complicated
+ systems it is very hard to get right, even for experts.
+
+ One of the sore spots of explicit names is comparing terms up
+ $\alpha$-renaming, which again generates a huge amounts of
+ substitutions and requires special care. We can represent the
+ relationship between variables and their binders, by...
+
+\item[Nameless] ...getting rid of names altogether, and representing
+ bound variables with an index referring to the `binding' structure, a
+ notion introduced by \cite{de1972lambda}. Classically $0$ represents
+ the variable bound by the innermost binding structure, $1$ the
+ second-innermost, and so on. For instance with simple abstractions we
+ might have
+ \[\mymacol{red}{\lambda}\, (\mymacol{blue}{\lambda}\, \mymacol{blue}{0}\, (\mymacol{AgdaInductiveConstructor}{\lambda\, 0}))\, (\mymacol{AgdaFunction}{\lambda}\, \mymacol{red}{1}\, \mymacol{AgdaFunction}{0}) : ((\mytya \myarr \mytya) \myarr \mytyb) \myarr \mytyb \]
+
+ While this technique is obviously terrible in terms of human
+ usability,\footnote{With some people going as far as defining it akin
+ to an inverse Turing test.} it is much more convenient as an
+ internal representation to deal with terms mechanically---at least in
+ simple cases. Moreover, $\alpha$ renaming ceases to be an issue, and
+ term comparison is purely syntactical.
+
+ Nonetheless, more complex, more complex constructs such as pattern
+ matching put some strain on the indices and many systems end up using
+ explicit names anyway (Agda, Coq, \dots).
+
+\end{description}
+
+In the past decade or so advancements in the Haskell's type system and
+in general the spread new programming practices have enabled to make the
+second option much more amenable. \mykant\ thus takes the second path
+through the use of Edward Kmett's excellent \texttt{bound}
+library.\footnote{Available at
+\url{http://hackage.haskell.org/package/bound}.} We decribe its
+advantages but also pitfalls in the previously relatively unknown
+territory of dependent types---\texttt{bound} being created mostly to
+handle more simply typed systems.
+
+\texttt{bound} builds on two core ideas. The first is the suggestion by
+\cite{Bird1999} consists of parametrising the term type over the type of
+the variables, and `nest' the type each time we enter a scope. If we
+wanted to define a term for the untyped $\lambda$-calculus, we might
+have
+\begin{Verbatim}
+data Void
+
+data Var v = Bound | Free v
+
+data Tm v
+ = V v -- Bound variable
+ | App (Tm v) (Tm v) -- Term application
+ | Lam (Tm (Var v)) -- Abstraction
+\end{Verbatim}
+Closed terms would be of type \texttt{Tm Void}, so that there would be
+no occurrences of \texttt{V}. However, inside an abstraction, we can
+have \texttt{V Bound}, representing the bound variable, and inside a
+second abstraction we can have \texttt{V Bound} or \texttt{V (Free
+Bound)}. Thus the term $\myabs{\myb{x}}{\myabs{\myb{y}}{\myb{x}}}$ could be represented as
+\begin{Verbatim}
+Lam (Lam (Free Bound))
+\end{Verbatim}
+This allows us to reflect at the type level the `nestedness' of a type,
+and since we usually work with functions polymorphic on the parameter
+\texttt{v} it's very hard to make mistakes by putting terms of the wrong
+nestedness where they don't belong.
+
+Even more interestingly, the substitution operation is perfectly
+captured by the \verb|>>=| (bind) operator of the \texttt{Monad}
+typeclass:
+\begin{Verbatim}
+class Monad m where
+ return :: m a
+ (>>=) :: m a -> (a -> m b) -> m b
+
+instance Monad Tm where
+ -- `return'ing turns a variable into a `Tm'
+ return = V
+
+ -- `t >>= f' takes a term `t' and a mapping from variables to terms
+ -- `f' and applies `f' to all the variables in `t', replacing them
+ -- with the mapped terms.
+ V v >>= f = f v
+ App m n >>= f = App (m >>= f) (n >>= f)
+
+ -- `Lam' is the tricky case: we modify the function to work with bound
+ -- variables, so that if it encounters `Bound' it leaves it untouched
+ -- (since the mapping referred to the outer scope); if it encounters a
+ -- free variable it asks `f' for the term and then updates all the
+ -- variables to make them refer to the outer scope they were meant to
+ -- be in.
+ Lam s >>= f = Lam (s >>= bump)
+ where bump Bound = return Bound
+ bump (Free v) = f v >>= V . Free
+\end{Verbatim}
+With this in mind, we can define functions which will not only work on
+\verb|Tm|, but on any \verb|Monad|!
+\begin{Verbatim}
+-- Replaces free variable `v' with `m' in `n'.
+subst :: (Eq v, Monad m) => v -> m v -> m v -> m v
+subst v m n = n >>= \v' -> if v == v' then m else return v'
+
+-- Replace the variable bound by `s' with term `t'.
+inst :: Monad m => m v -> m (Var v) -> m v
+inst t s = do v <- s
+ case v of
+ Bound -> t
+ Free v' -> return v'
+\end{Verbatim}
+The beauty of this technique is that in a few simple function we have
+defined all the core operations in a general and `obviously correct'
+way, with the extra confidence of having the type checker looking our
+back.
+
+Moreover, if we take the top level term type to be \verb|Tm String|, we
+get for free a representation of terms with top-level, definitions;
+where closed terms contain only \verb|String| references to said
+definitions---see also \cite{McBride2004b}.
+
+What are then the pitfalls of this seemingly invincible technique? The
+most obvious impediment is the need for polymorphic recursion.
+Functions traversing terms parametrised by the variable type will have
+types such as
+\begin{Verbatim}
+-- Infer the type of a term, or return an error.
+infer :: Tm v -> Either Error (Tm v)
+\end{Verbatim}
+When traversing under a \verb|Scope| the parameter changes from \verb|v|
+to \verb|Var v|, and thus if we do not specify the type for our function explicitly
+inference will fail---type inference for polymorphic recursion being
+undecidable \citep{henglein1993type}. This causes some annoyance,
+especially in the presence of many local definitions that we would like
+to leave untyped.
+
+But the real issue is the fact that giving a type parametrised over a
+variable---say \verb|m v|---a \verb|Monad| instance means being able to
+only substitute variables for values of type \verb|m v|. This is a
+considerable inconvenience. Consider for instance the case of
+telescopes, which are a central tool to deal with contexts and other
+constructs:
+\begin{Verbatim}
+data Tele m v = End (m v) | Bind (m v) (Tele (Var v))
+type TeleTm = Tele Tm
+\end{Verbatim}
+The problem here is that what we want to substitute for variables in
+\verb|Tele m v| is \verb|m v| (probably \verb|Tm v|), not \verb|Tele m v| itself! What we need is
+\begin{Verbatim}
+bindTele :: Monad m => Tele m a -> (a -> m b) -> Tele m b
+substTele :: (Eq v, Monad m) => v -> m v -> Tele m v -> Tele m v
+instTele :: Monad m => m v -> Tele m (Var v) -> Tele m v
+\end{Verbatim}
+Not what \verb|Monad| gives us. Solving this issue in an elegant way
+has been a major sink of time and source of headaches for the author,
+who analysed some of the alternatives---most notably the work by
+\cite{weirich2011binders}---but found it impossible to give up the
+simplicity of the model above.
+
+That said, our term type is still reasonably brief, as shown in full in
+Figure \ref{fig:term}. The fact that propositions cannot be factored
+out in another data type is a consequence of the problems described
+above. However the real pain is during elaboration, where we are forced
+to treat everything as a type while we would much rather have
+telescopes. Future work would include writing a library that marries a
+nice interface similar to the one of \verb|bound| with a more flexible
+interface.
+
+\begin{figure}[t]
+{\small\begin{verbatim}-- A top-level name.
+type Id = String
+-- A data/type constructor name.
+type ConId = String
+
+-- A term, parametrised over the variable (`v') and over the reference
+-- type used in the type hierarchy (`r').
+data Tm r v
+ = V v -- Variable.
+ | Ty r -- Type, with a hierarchy reference.
+ | Lam (TmScope r v) -- Abstraction.
+ | Arr (Tm r v) (TmScope r v) -- Dependent function.
+ | App (Tm r v) (Tm r v) -- Application.
+ | Ann (Tm r v) (Tm r v) -- Annotated term.
+ -- Data constructor, the first ConId is the type constructor and
+ -- the second is the data constructor.
+ | Con ADTRec ConId ConId [Tm r v]
+ -- Data destrutor, again first ConId being the type constructor
+ -- and the second the name of the eliminator.
+ | Destr ADTRec ConId Id (Tm r v)
+ -- A type hole.
+ | Hole HoleId [Tm r v]
+ -- Decoding of propositions.
+ | Dec (Tm r v)
+
+ -- Propositions.
+ | Prop r -- The type of proofs, with hierarchy reference.
+ | Top
+ | Bot
+ | And (Tm r v) (Tm r v)
+ | Forall (Tm r v) (TmScope r v)
+ -- Heterogeneous equality.
+ | Eq (Tm r v) (Tm r v) (Tm r v) (Tm r v)
+
+-- Either a data type, or a record.
+data ADTRec = ADT | Rec
+
+-- Either a coercion, or coherence.
+data Coeh = Coe | Coh\end{verbatim}
+}
+ \caption{Data type for terms in \mykant.}
+ \label{fig:term}
+\end{figure}
+
+We also make use of a `forgetful' data type (as provided by
+\verb|bound|) to store user-provided variables names along with the
+`nameless' representation, so that the names will not be considered when
+compared terms, but will be available when distilling so that we can
+recover variable names that are as close as possible to what the user
+originally used.
+
+\subsubsection{Context}
+
+% TODO finish