+efficiently with disjoint set data structure, and is crucial to keep the
+graph compact, given the very large number of constraints generated when
+type checking.
+
+\subsection{(Web) REPL}
+
+Finally, we take a break from the types by giving a brief account of the
+design of our REPL, being a good example of modular design using various
+constructs dear to the Haskell programmer.
+
+Across our codebase we make use of a \emph{monad transformers} named
+\texttt{KMonadT}. Without delving into the details of \texttt{KMonadT}
+or of monad transformers,\footnote{See
+ \url{https://en.wikibooks.org/wiki/Haskell/Monad_transformers.}}
+computation done inside \texttt{KMonadT} can easily retrieve and modify
+the environment and throw various kind of errors, be them parse error,
+type errors, etc. Moreover, \texttt{KMonadT} being a monad
+\emph{transformers}, we can `plug in' other monads to have access to
+other facilities, such as input/output.
+
+That said, the REPL is represented as a function in \texttt{KMonadT}
+consuming input and hopefully producing output. Then, frontends can
+very easily written by marshalling data in and out of the REPL:
+\begin{Verbatim}
+data Input
+ = ITyCheck String -- Type check a term
+ | IEval String -- Evaluate a term
+ | IDecl String -- Declare something
+ | ...
+
+data Output
+ = OTyCheck TmRefId [HoleCtx] -- Type checked term, with holes
+ | OPretty TmRefId -- Term to pretty print, after evaluation
+ | OHoles [HoleCtx] -- Just holes, classically after loading a file
+ | ...
+
+-- KMonadT is parametrised over the type of the variables, which depends
+-- on how deep in the term structure we are. For the REPL, we only deal
+-- with top-level terms, and thus only `Id' variables---top level names.
+type REPL m = KMonadT Id m
+
+repl :: ReadFile m => Input -> REPL m Output
+\end{Verbatim}
+The \texttt{ReadFile} monad embodies the only `extra' action that we
+need to have access too when running the REPL: reading files. We could
+simply use the \texttt{IO} monad, but this will not serve us well when
+implementing front end facing untrusted parties accessing the application
+running on our servers. In our case we expose the REPL as a web
+application, and we want the user to be able to load only from a
+pre-defined directory, not from the entire file system.
+
+For this reason we specify \texttt{ReadFile} to have just one function:
+\begin{Verbatim}
+class Monad m => ReadFile m where
+ readFile' :: FilePath -> m (Either IOError String)
+\end{Verbatim}
+While in the command-line application we will use the \texttt{IO} monad
+and have \texttt{readFile'} to work in the `obvious' way---by reading
+the file corresponding to the given file path---in the web prompt we
+will have it to accept only a file name, not a path, and read it from a
+pre-defined directory:
+\begin{Verbatim}
+-- The monad that will run the web REPL. The `ReaderT' holds the
+-- filepath to the directory where the files loadable by the user live.
+-- The underlying `IO' monad will be used to actually read the files.
+newtype DirRead a = DirRead (ReaderT FilePath IO a)
+
+instance ReadFile DirRead where
+ readFile' fp =
+ do -- We get the base directory in the `ReaderT' with `ask'
+ dir <- DirRead ask
+ -- Is the filepath provided an unqualified file name?
+ if snd (splitFileName fp) == fp
+ -- If yes, go ahead and read the file, by lifting
+ -- `readFile'' into the IO monad
+ then DirRead (lift (readFile' (dir </> fp)))
+ -- If not, return an error
+ else return (Left (strMsg ("Invalid file name `" ++ fp ++ "'")))
+\end{Verbatim}
+Once this light-weight infrastructure is in place, adding a web
+interface was an easy exercise. We use Jasper Van der Jeugt's
+\texttt{websockets} library\footnote{Available at
+ \url{http://hackage.haskell.org/package/websockets}.} to create a proxy
+that receives JSON messages with the user input, turns them into
+\texttt{Input} messages for the REPL, and then sends back a JSON message
+with the response. Moreover, each client is handled in a separate
+threads, so crashes of the REPL in single threads will not bring the
+whole application down.
+
+On the clients side, we had to write some JavaScript to accept input
+from a form, and to make the responses appear on the screen. The web
+prompt is publicly available at \url{http://bertus.mazzo.li}, a sample
+session is shown Figure \ref{fig:web-prompt-one}.