#+TITLE: Exceptionally Monadic Error Handling
#+SUBTITLE: Looking at @@tex:$bind$@@ and squinting really hard
#+AUTHOR: Jan Malakhovski
#+EMAIL: papers@oxij.org
#+EMAIL-COMMENT: preferably with paper title in the subject line
#+AFFIL: IRIT, University of Toulouse-3 and ITMO University
#+DATE: February 2014 - October 2018
#+BEGIN_abstract
We notice that the type of
src_haskell{catch :: c a -> (e -> c a) -> c a}
operator is a special case of monadic src_haskell{bind} operator
src_haskell{(>>=) :: m a -> (a -> m b) -> m b},
the semantics (surprisingly) matches, and this observation has many
interesting consequences.
For instance, the reader is probably aware that the monadic essence of
the src_haskell{(>>=)} operator of the error monad
$\lambda A.E \lor A$
is to behave like identity monad for "normal" values and to stop on
"errors". The unappreciated fact is that handling of said "errors"
with a src_haskell{catch} operator of the "flipped" "conjoined" error
monad
$\lambda E.E \lor A$
is, too, a monadic computation that treats still unhandled "errors" as
"normal" values and stops when an "error" is finally handled.
We show that for an appropriately indexed type of computations such a
"conjoined" structure naturally follows from the conventional
operational semantics of src_haskell{throw} and src_haskell{catch}
operators. Consequently, we show that this structure uniformly
generalizes /all/ conventional monadic error handling mechanisms we
are aware of. We also demonstrate several more interesting instances
of this structure of which at least bi-indexed monadic parser
combinators and conventional exceptions implemented via continuations
have immediate practical applications. Finally, we notice that these
observations provide surprising perspectives on error handling in
general and point to a largely unexplored trail in programming
language design space.
#+END_abstract
@@tex:\small\tableofcontents\normalsize\newpage@@
* Extended Abstract
@@tex:\label{sec:extabstract}@@
In this article we shall use Haskell programming language extensively
for the purposes of precise expression of thought (including Haskell
type class names for the names of the respective algebraic structures
where appropriate, e.g. "src_haskell{Monad}" instead of "monad").
- We note that the types of
#+BEGIN_SRC haskell-spec
throw :: e -> c a
catch :: c a -> (e -> c a) -> c a
#+END_SRC
operators are special cases of src_haskell{Monad}ic
src_haskell{return} and src_haskell{(>>=)} (src_haskell{bind})
operators
#+BEGIN_SRC haskell-spec
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
#+END_SRC
(substitute $[a \mapsto e, m \mapsto \lambda\_.c~a]$ into their
types, see \cref{sec:init,sec:type-of-catch}).
- Hence, a type of computations src_haskell{c e a} with two indexes
where src_haskell{e} signifies a type of errors and src_haskell{a}
signifies a type of values can be made a src_haskell{Monad} twice:
once for src_haskell{e} and once for src_haskell{a}.
#+BEGIN_SRC haskell-spec
class ConjoinedMonads c where
return :: a -> c e a
(>>=) :: c e a -> (a -> c e b) -> c e b
throw :: e -> c e a
catch :: c e a -> (e -> c f a) -> c f a
#+END_SRC
Moreover, for such a structure src_haskell{throw} is a left zero for
src_haskell{(>>=)} and src_haskell{return} is a left zero for
src_haskell{catch} (see \cref{sec:conjoinedly-monadic,sec:logical}).
- We prove that the type of the above src_haskell{catch} is most
general type for any src_haskell{Monad}ic structure
src_haskell{\a -> c e a}
with additional src_haskell{throw} and src_haskell{catch} operators
satisfying conventional operational semantics (via simple
unification of types for several equations that follow from
semantics of said operators, see \cref{sec:type-of-catch}). Or,
dually, we prove that src_haskell{(>>=)} has the most general type
for expressing sequential computations for src_haskell{Monad}ic
structure
src_haskell{\e -> c e a}
(with operators named src_haskell{throw} and src_haskell{catch})
with additional src_haskell{return} and src_haskell{(>>=)} operators
satisfying conventional operational semantics (see
footnote~\ref{fn:its-dual}).
- Substituting a src_haskell{Const}ant src_haskell{Functor} for
src_haskell{c} into src_haskell{ConjoinedMonads} above (i.e., fixing
the type of errors) produces the definition of
src_haskell{MonadError}, and, with some equivalent redefinitions,
src_haskell{MonadCatch} (see \cref{sec:instances:constant}).
Similarly, src_haskell{IO} with similar redefinitions and with the
usual caveats of \cref{rem:io-caveats} is a
src_haskell{ConjoinedMonads} instance too (see
\cref{sec:instances:io}).
- src_haskell{ExceptT} (\cref{sec:instances:either}) and some other
lesser known and potentially novel concrete structures (see all
sections with "Instance:" in the title, most interestingly,
\cref{sec:instances:throw-catch-cc}) have operators of such types
and their semantics matches (or they can be redefined in an
equivalent way such that the core part of the resulting structure
then matches) the semantics of src_haskell{Monad} exactly.
- src_haskell{Monad} type class has a well-known "fish" representation
where "src_haskell{bind}" src_haskell{(>>=)} operator is replaced by
"src_haskell{fish}" operator
#+BEGIN_SRC haskell-spec
(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
#+END_SRC
and src_haskell{Monad} laws are just monoidal laws.
Hence, all those structures can be seen as a pairs of monoids over
bi-indexed types with identity elements for respective
src_haskell{bind}s as left zeros for conjoined src_haskell{bind}s
(\cref{sec:conjoinedly-monadic}). We find this symmetry to be
hypnotic and generalize it in \cref{sec:applicatives}.
- The answer to "Why didn't anyone notice this already?" seems to be
that this structure cannot be expressed well in Haskell (see
\cref{sec:encodings}).
- Meanwhile, it has at least several practically useful instances:
- Parser combinators that are precise about errors they produce and
that reuse common src_haskell{Monad}ic combinators for both
parsing and handling of errors. For instance, the type of
src_haskell{many} for such a parser combinator guarantees that it
cannot throw any errors
#+BEGIN_SRC haskell-spec
many :: c e a -> c f [a]
#+END_SRC
(since src_haskell{f} can be anything, it cannot be anything in
particular) and
#+BEGIN_SRC haskell-spec
choice :: [c e a] -> c e a
#+END_SRC
is an instance of src_haskell{foldM} (see
\cref{sec:instances:parser-combinators}).
# TODO(low): use a better example instance?
- Conventional exceptions expressed using src_haskell{Reader}
src_haskell{Monad} and second-rank src_haskell{callCC} (the whole
idea of which seems to be novel, see
\cref{sec:instances:throw-catch-cc}).
- Error-explicit src_haskell{IO} (\cref{sec:instances:eio}), the
latter and similar structures with similar motivation were
proposed before, but they did not use the fact that their "other
half" is a src_haskell{Monad} too.
Every item on the above list, to our best knowledge, is a headline
contribution.
* Preliminaries
@@tex:\label{sec:preliminaries}@@
Most of the results of this paper are
**language-agnostic** and can be applied (if not straight to practice,
then at least to inform design choices) to any programming
language (that permits at least two computationally distinguishable
program states and some kind of dynamic control flow control) as our
definition of an "/error/" in "error handling" is just "an abnormal
program state causing execution of an abnormal code path" and both
"abnormal"s can be arbitrarily defined (see footnote~\ref{fn:terms}).
While most of our results are applicable to any programming language,
we need /some/ language to express them in and Haskell seems to be the
most natural choice to host this discussion since
- most of the cited literature uses Haskell or some variant of ML;
- it has the largest number of error handling mechanisms in active
use of all the programming languages we are aware of;
- as a consequence, most other programming languages implement a
subset of Haskell's enormous library of error handling
mechanisms;
- while it is not ideal for our purposes (Haskell cannot properly
express the main result and the improper encoding of the main result
is not particularly convenient, see \cref{sec:encodings}), it is
expressive enough to show how a convenient encoding could have been
implemented in theory;
- it is surprisingly popular for an "academic" language.
Using Haskell also allows this paper to be encoded as a set of
Literate Haskell programs in a single Emacs Org-Mode
tree~\cite{OrgMode,Schulte:2011:MLCELPRR}.[fn::The source code is
available at [[https://oxij.org/paper/ExceptionallyMonadic/]].
@@tex:\ifnum 0\ifpdf 1\fi\ifxetex 1\fi\ifluatex 1\fi=0@@
It also gets embedded into the PDF version of this article when the
source gets compiled straight to PDF (i.e. via =pdftex=, =xetex=, or
=luatex=, but not via =dvipdf=). Unfortunately, the file you are
looking at was compiled using =dvipdf=. This also means that in this
file URLs with line breaks would not be clickable as =dvipdf=
generates incorrect PDF link boxes for them. Properly compiled version
is available via the above link.
@@tex:\else
It is also embedded straight into the PDF version of this article
(click here \attachfile{article.org} or look for "attachments" in
your PDF viewer).\fi@@]
# By the way, to extract the tangled source files you can run
# $ emacs --batch --eval "(progn (require 'ob-tangle) (org-babel-tangle-file \"article.org\"))"
# from the shell. It would generate a bunch of tng-*.hs files.
Our preferred compiler is The Glorious Glasgow Haskell Compiler
(GHC)~\cite{GHC} version 8.2 as we shall use a number of its
extensions over Haskell 2010~\cite{Haskell2010} specification.
Readers unfamiliar with Haskell are advised to read through any
tutorial introduction into Haskell at least until they start feeling
like Haskell is just a syntax for school-level arithmetic with
user-definable functions, lambdas, types, algebraic data types and type
classes. After that it is recommended to look over
Typeclassopedia~\cite{HaskellWiki:Typeclassopedia}, Diehl's
web-page~\cite{Diehl:2016:WIW}, the table of contents (just the list
of modules) of GHC's =base= package~\cite{Hackage:base4900}, and the
types and descriptions of functions from the src_haskell{Prelude}
module of =base=.
The rest can be learned on-demand from
\cref{sec:tutorial:basic,sec:tutorial:non-basic} and cited
documentation.
* Introduction
#+BEGIN_definition
@@tex:\label{dfn:error-handling}@@
Generally, when program encounters an "/error/" all it can do is to
switch to an "/exceptional/" execution path~\cite{Benton:2001:ES}. The
latter can then either encounter an "/error/" itself or
1. @@tex:\label{c:a}@@ gracefully "/terminate/" some part of the
previous computation (including the whole program as a degenerate
case) and continue (when there is something left to continue),
2. @@tex:\label{c:b}@@ "/fix/" the "/problem/" and resume the
computation as if nothing has happened.
#+END_definition
\emph{Error handling}[fn::@@tex:\label{fn:terms}@@Not a consensus
term. Some people would disagree with this choice of a name as they
would not consider some of our examples below to be about "errors".
However, for the purposes of this article we opted into generalizing
the term "/error/" of "error handling" instead of inventing new
terminology or appropriating terminology like "exceptions",
"interrupts", "conditions" or "effects" that has other very specific
uses. To see the problem with the conventional terminology consider
how would you define "program encountered an error" formally and
generally for *any* abstract interpreter (you can not). Now consider
the case where an interpreter is a tower of interpreters interpreting
one another. Clearly, what is an "/error/" for one interpreter can be
considered normal execution for the one below. A simple example of
such a structure is the src_haskell{Maybe} src_haskell{Monad}
discussed in \cref{sec:maybe} in which expressions using
src_haskell{do}-syntax never consider src_haskell{Nothing}s while
handling of said src_haskell{Nothing}s by the src_haskell{Monad}ic
src_haskell{(>>=)} operator is a completely ordinary src_haskell{case}
for the underlying Haskell interpreter. Hence, in this article we
consider anything that matches \cref{dfn:error-handling} to be about
\emph{"error" handling}. If the reader still feels like disagreeing
with our argument we advise mentally substituting every our use of
"error" with something like "an abnormal program state causing
execution of an abnormal code path" (where definitions of both
"abnormal"s are interpreter-specific).] is an algebraic subfield of
the programming languages theory that studies this sort of seemingly
simple control structures.
Different substitutions for "/error/", "/exceptional/" and
"/terminate/" into \cref{dfn:error-handling} variant~\ref{c:a} and
substitutions for "/error/", "/exceptional/", "/fix/" and "/problem/"
into \cref{dfn:error-handling} variant~\ref{c:b} produce different
error handling mechanisms. Some examples:
- Identity substitution for variant~\ref{c:a} gives programming with
error codes, programming with algebraic
data types~\cite{burstall-hope-80, Bailey:1985:HT} that encode
errors, programming with algebraic data types with
errors~\cite{ADJ76, Gogolla:1984:AOS} (not the same thing),
exceptions in conventional programming
languages~\cite{Goodenough:1975:EHI, Goodenough:1975:EHD,
Goldberg:1983:SLI, Koenig:1990:EHC, Benton:2001:ES} (with so called
"termination semantics"~\cite[16.6 Exception Handling: Resumption
vs. Termination]{Stroustrup:DEC94}), error handling with
monads~\cite{moggi-89, moggi-91, Wadler:1992:EFP,
Swierstra:2008:DTL, Iborra:2010:ETE, Katsumata:2014:PEM}, monad
transformers~\cite{Liang:1995:MTM, Benton:2002:ME,
Hackage:transformers0520}, Scheme's and ML's
src_scheme{call/cc}~\cite{Sperber:2010:RnRS}, and delimited
src_scheme{callCC}~\cite{Asai:2011:IPS, Kiselyov:2012:AAC,
Hackage:transformers0520}.
- Substituting "/unparsable string/", "/alternative/", "/backtrack/"
for variant~\ref{c:a} gives monadic parser
combinators~\cite{Leijen:2001:PDS}.
- Identity substitution for variant~\ref{c:b} gives error handling in
languages with so called "resumption semantics"~\cite[16.6 Exception
Handling: Resumption vs. Termination]{Stroustrup:DEC94} like, for
instance, Common LISP~\cite{Pitman:2001:CHL} (/condition handling/)
and Smalltalk~\cite{Goldberg:1983:SLI}.
- Substituting "/effect/", "/effect handler/", /handle/", "/it/" for
variant~\ref{c:a} or~\ref{c:b} (depending on the details of the
calculus) produces effect systems~\cite{Benton:2002:ME,
Plotkin:2009:HAE, Brady:2013:PRA, Kammar:2013:HA, Kiselyov:2013:EEA,
Kiselyov:2015:FMM} and effect systems based on modal logic with
names~\cite{Nanevski:2004:FPNN, Nanevski:2005:MCEH}.
- "/System call/", "/system call handler/", "/handle/", "/it/" for
variant~\ref{c:b} produces conventional \emph{system
calls}~\cite{IEEE:2001:ISR}.[fn::Except in most
UNIX-like operating systems system calls cannot call other system
calls directly and have to use an equivalent kernel API
instead.][fn::Indeed, algebraic effects from the point of view of an
OS-developer are just properly typed system calls with nesting and
modular handling.]
- Substituting "/signal/", "/signal handler/", "/handle/", "/it/",
"/it/" for variant~\ref{c:b} gives hardware interrupts and POSIX
signals~\cite{IEEE:2001:ISR}.[fn::Indeed, POSIX
signals and hardware interrupts are "system calls in reverse" (with
some complications outside of the scope of this article): kernel
and/or hardware raises and applications handle them.]
The first complication of the above scheme is the question of whenever
for a given error handling mechanism the "/error/" raising
operator
1. passes control to a statically selected (lexically closest or
explicitly specified) enclosing error handling construct (e.g.
src_elisp{throw} and src_elisp{catch} in Emacs
LISP~\cite{Emacs:ELRM:Catch-and-Throw}, POSIX system calls and
signals) or
2. the language does dynamic dispatch to select an appropriate
error handler (like exceptions in most conventional languages
like C++, Java, Python, etc do).
Another complication is ordering:
1. Most conventional programming languages derive their error handling
from SmallTalk~\cite{Goldberg:1983:SLI} and Common
LISP~\cite{Pitman:2001:CHL} and the order in which the program
handles "/errors/" corresponds to the order in which execution
encounters them.
2. Meanwhile, some CPU ISAs[fn::Instruction Set Architecture (ISA) is
a specification that describes a set of Operation Codes (OPcodes,
which are a binary representation of an assembly language) with
their operational semantics. "i386", "i686", "amd64"
("@@tex:x86\_64@@"), "aarch64", "riscv64", etc are ISAs.] expose
the internal non-determinism and allow different independent
data-flows to produce hardware exceptions in non-deterministic
manner (e.g. arithmetic instructions on DEC Alpha). So do
Haskell~\cite{PeytonJones:1999:SIE} (see \cref{sec:imprecise}) and,
to some extent, C++~\cite{CFAQ:SeqPoints} programming languages.
# TODO(low): I'd like to cite something for DEC Alpha ASM, but can't find
# anything citable
Finally, another dimension of the problem is whenever the objects
signifying "/errors/" (e.g. arguments of src_haskell{throw}) are
1. first-class values (error codes, algebraic data types) as in most
conventional languages,
2. labels or tags as in modal logic with names and, to some degree,
with src_scheme{call/cc} and src_haskell{callCC}.
In short, despite its seemingly simple operational semantics, error handling
is an algebraically rich field of programming languages theory.
Meanwhile, from the perspective of types there are several schools of
thought about effects.
- The first one, started by Gifford and
Lucassen~\cite{Gifford:1986:IFI, Lucassen:1987:TE,
lucassen-gifford-88} represents effects as type annotations. This
works well in programming languages with eager evaluation, but
becomes complicated in lazy languages (application in a lazy
language delays effects until thunk's evaluation, hence type system
has to either put nontrivial restrictions on the use of effects in
expressions or annotate both arrows and values with effects, the
latter, among other things, breaks type preservation of
$\eta$-conversion since $\lambda x . f x$ moves effect annotation
from the arrow to the result type).
- The second one, started by Moggi and
Wadler~\cite{moggi-89,Wadler:1992:EFP} confines effects to monadic
computations. The latter can then be annotated with effect
annotations themselves~\cite{wadler-thiemann-03}. Monads work well
for small programs with a small number of effects, but, it is
commonly argued, they don't play as nice in larger programs
because they lack in modularity~\cite{Brady:2013:PRA} (hence, the
need for monad transformers, which are then critiqued as hard to
tame~\cite{Kiselyov:2013:EEA}) and produce languages with
non-uniform syntax (pure functions look very different from monadic
ones and functions that are useful in both contexts have to be
duplicated, think e.g. src_haskell{map} and src_haskell{mapM}).
- The third one, started by Nanevski~\cite{Nanevski:2004:FPNN}
represents effects using modal logic with names. Practical
consequences of this way of doing things are unknown, as this
construction didn't get much adoption yet.
In short, from type-theoretic point of view the progression of topics
in the cited literature can be seen as pursuing calculi that are, at
the same time, computationally efficient, algebraically simple (like
monads), but modular (like effect systems).
Note, however, that all of those schools of thought consider
exceptions to be effects, they only disagree about the way to
represent the latter. Meanwhile, from a perspective of a programming
language implementer, there are several problems with that world view:
- mechanisms that support resumption semantics are commonly
disregarded as useless and computationally expensive error handling
mechanisms (most notably~\cite[16.6 Exception Handling: Resumption
vs. Termination, pp. 390–393]{Stroustrup:DEC94}),
- in particular, all popular programming languages implement builtin
exceptions even though they have more general error handling
mechanisms like /condition handling/ in Common LISP and
src_scheme{call/cc} in Scheme and ML because those are just too
computationally expensive for emulation of conventional
exceptions~\cite{Kiselyov:2012:AAC},
- and even in languages with nothing but exceptions and termination
semantics, high-performance libraries that do a lot of error
handling frequently prefer not to use exceptions for performance
reasons and to remove any non-local control-flow.
In short, from practical point of view /most/ of those type-theoretic
constructs are an overkill for /most/ programs. Meanwhile, we are not
aware of any non-ad-hoc language-agnostic algebraic structure that
captures all of the exception handling (both src_haskell{throw}ing,
and src_haskell{catch}ing) without introducing any other superfluous
structure on top. In this article we shall demonstrate a fairly
straightforward but surprisingly useful solution to this problem.
* Not a Tutorial: Side A
@@tex:\label{sec:tutorial:basic}@@
While algebraic structures used in this article are simple, there are
a lot of them. This section is intended as a reference point for all
algebraic structures relevant in the context of error handling that
are referenced in the rest of the paper (for reader's convenience and
for high self-sufficiency of the Literate Haskell version). Most of
those are usually assumed to be common knowledge among Haskell
programmers. Note however, that this section is not intended to be a
tutorial on either
- functional/declarative programming in general,
- Haskell language in particular (see \cref{sec:preliminaries} for
pointers),
- error handling in Haskell in general,
- practical usage of error handling structures discussed is this
section in particular (we show only very primitive examples, if any;
for the interesting ones the reader will have to look into citations
and examples given in the original sources).
All structures of this section are ordered from semantically simple to
more complex (that is, we do not topologically sort them by their
dependencies in GHC sources). For the reasons of simplicity, uniformity,
self-containment, and novel perspective some of the given
definitions differ slightly from (but are isomorphic/equivalent to)
the versions provided by their original authors. The most notable
difference is the use of src_haskell{Pointed} type class (see
\cref{sec:applicative-functor}) instead of conventional
src_haskell{Monad}ic src_haskell{return} and src_haskell{Applicative}
src_haskell{pure}. All structures are listed alongside references to
the corresponding papers, documentation and original source code.
This section can be boring (although, we feel like most remarks and
footnotes are not). On the first reading we advise to skip straight to
\cref{sec:tutorial:non-basic} and refer back to this section on
demand.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
{-# LANGUAGE NoImplicitPrelude, StandaloneDeriving, MagicHash, UnboxedTuples, RebindableSyntax #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances #-}
-- If you are reading this, note the RebindableSyntax extension. We
-- actually redefine `Monad` class in this module and all `do`s use
-- our version of (>>=), not the builtin one. Pretty cool, right?
-- Borrow some stuff
import GHC.Prim (State#, RealWorld)
import Prelude ((.), ($), id, const, Bool(..), Char(..), String, (++), Int, Show(..), Num(..), Eq(..), (&&))
import Data.Typeable (Typeable(..))
import Data.List (foldr, foldl')
import qualified GHC.Prim as GP
import qualified GHC.Types as GT
import qualified Prelude as P
import qualified Data.Typeable as T
import qualified Control.Monad as M
-- RebindableSyntax also allows to rebind `if`s, but we are ok with
-- the default one
ifThenElse True b c = b
ifThenElse False b c = c
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs :exports none
{-# LANGUAGE StandaloneDeriving, MagicHash, RankNTypes #-}
-- This file is only used for syntax checking, it's ok if this doesn't typecheck and compile
#+END_SRC
** Before-src_haskell{Monad}ic
This subsection describes type classes that have less structure than
src_haskell{Monad} but are useful for error handling nevertheless.
*** src_haskell{Monoid}
src_haskell{GHC.Base} from =base=~\cite{Hackage:base4900} package
defines src_haskell{Monoid} type class as
follows[fn::@@tex:\label{fn:monoid-split}@@Note that by following
src_haskell{Pointed} logic used below we should have split
src_haskell{Monoid} into two type classes, but since we will not use
src_haskell{Monoid}s that much in the rest of the article we shall use
the original definition as is.]
#+BEGIN_SRC haskell :tangle tng-main.hs
class Monoid a where
mempty :: a
mappend :: a -> a -> a
-- defined for performance reasons
mconcat :: [a] -> a
mconcat = foldr mappend mempty
#+END_SRC
\noindent and wants its instances to satisfy the following
conventional equations ("src_haskell{Monoid} laws")
#+BEGIN_SRC haskell-spec
-- `mempty` is left identity for `mappend`,
mempty `mappend` x == x
-- `mempty` is right identity for `mappend`,
x `mappend` mempty == x
-- `mappend` is associative,
x `mappend` (y `mappend` z)
== (x `mappend` y) `mappend` z
#+END_SRC
\noindent and an additional constraint
#+BEGIN_SRC haskell-spec
-- and `mconcat` is extensionally
-- equal to its default implementation
mconcat == foldr mappend mempty
#+END_SRC
Signature and default implementation for src_haskell{mconcat} is
defined in the type class because src_haskell{mconcat} is a commonly
used function that has different extensionally equal intensionally
non-equal definitions with varied performance trade-offs. For
instance,
#+BEGIN_SRC haskell :tangle tng-main.hs
mconcat' :: Monoid a => [a] -> a
mconcat' = foldl' mappend mempty
#+END_SRC
\noindent (where src_haskell{foldl'} is a strict left fold) is
another definition that satisfies the law given above (since
src_haskell{mappend} is associative), but this implementation will
not produce any superfluous thunks for strict src_haskell{mappend}.
src_haskell{Monoid}s are not designed for error handling per se but
programmers can use their neutral elements to represent an error and
associative composition to ignore them. Whenever "ignoring" is
"handling" is a matter of personal taste.
One of the simpler instances is, of course, a list
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Monoid [a] where
mempty = []
mappend = (++)
#+END_SRC
\noindent and hence, for instance, functions generating errors can
produce empty lists on errors and singleton lists on successes.
*** src_haskell{Functor}, src_haskell{Pointed}, src_haskell{Applicative}
@@tex:\label{sec:applicative-functor}@@
@@tex:\label{sec:identity}@@
Most of the error handling mechanisms that follow are
src_haskell{Applicative} src_haskell{Functor}s. src_haskell{GHC.Base}
from =base=~\cite{Hackage:base4900} package defines those two
algebraic structures as follows
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
class Functor f where
fmap :: (a -> b) -> f a -> f b
infixl 4 <*>
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
#+END_SRC
\noindent and wants their instances to satisfy
#+BEGIN_SRC haskell-spec
-- `fmap` preserves identity
fmap id == id
-- `(<*>)` is `fmap` for pure functions
pure f <*> x == fmap f x
#+END_SRC
\noindent and some more somewhat more complicated
equations~\cite{HaskellWiki:Typeclassopedia}. We shall ignore those
for the purposes of this article (we will never use them
explicitly). Meanwhile, for the purposes of this article we shall
split the src_haskell{pure} function out of src_haskell{Applicative}
into its own src_haskell{Pointed} type class and redefine
src_haskell{Applicative} using it as follows (this will simplify
some later definitions).
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- copy-paste
class Functor f where
fmap :: (a -> b) -> f a -> f b
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs
class Pointed f where
pure :: a -> f a
infixl 4 <*>
class (Pointed f, Functor f) => Applicative f where
(<*>) :: f (a -> b) -> f a -> f b
#+END_SRC
We shall give all definitions and laws using this hierarchy unless
explicitly stated otherwise.
The most trivial example of src_haskell{Applicative} is the
src_haskell{Identity} src_haskell{Functor} defined in
src_haskell{Data.Functor.Identity} of =base=
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype Identity a = Identity
{ runIdentity :: a }
instance Pointed Identity where
pure = Identity
instance Functor Identity where
fmap f (Identity a) = Identity (f a)
instance Applicative Identity where
(Identity f) <*> (Identity x) = Identity (f x)
#+END_SRC
The most trivial example of a src_haskell{Functor} that is not
src_haskell{Applicative} is src_haskell{Const}ant src_haskell{Functor}
defined in src_haskell{Data.Functor.Const} of =base= as
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype Const a b = Const
{ getConst :: a }
instance Functor (Const a) where
-- note that it changes type here
fmap f (Const a) = Const a
-- so the following would not work
-- fmap f x = x
#+END_SRC
\noindent It is missing a src_haskell{Pointed} instance. However, if
the argument of src_haskell{Const} is a src_haskell{Monoid} we can
define it as
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Monoid a => Pointed (Const a) where
pure a = Const mempty
instance Monoid a => Applicative (Const a) where
Const x <*> Const a = Const (mappend x a)
#+END_SRC
#+BEGIN_remark
@@tex:\label{rem:applicative-as-app}@@
One can think of src_haskell{Applicative f} as representing
/generalized function application/ on structure src_haskell{f}:
src_haskell{pure} lifts pure values into src_haskell{f} while
src_haskell{(<*>)} provides a way to apply functions to arguments over
src_haskell{f}. Note however, that src_haskell{Applicative} is not a
structure for representing /generalized functions/ (e.g.
src_haskell{Applicative} gives no way to compose functions or to
introduce lambdas, unlike the src_haskell{Monad}, see
\cref{rem:monad-as-app}).
#+END_remark
*** src_haskell{Alternative}
@@tex:\label{sec:alternative}@@
src_haskell{Control.Applicative} module of
=base=~\cite{Hackage:base4900} defines src_haskell{Alternative} class
as a monoid on src_haskell{Applicative}
src_haskell{Functor}s.\cref{fn:monoid-split}
#+BEGIN_SRC haskell :tangle tng-main.hs
class Applicative f => Alternative f where
empty :: f a
(<|>) :: f a -> f a -> f a
-- defined for performance reasons
some :: f a -> f [a]
some v = fmap (:) v <*> many v
many :: f a -> f [a]
many v = some v <|> pure []
#+END_SRC
\noindent requiring monoid laws to hold for src_haskell{empty} and
src_haskell{(<|>)}
#+BEGIN_SRC haskell-spec
-- `empty` is left identity for `(<|>)`,
empty <|> x == x
-- `empty` is right identity for `(<|>)`,
x <|> empty == x
-- `(<|>)` is associative,
x <|> (y <|> z)
== (x <|> y) <|> z
-- and both `some` and `many` are
-- extensionally equal to their
-- default implementations
some v == fmap (:) v <*> many v
many v == some v <|> pure []
#+END_SRC
Combinators src_haskell{some} and src_haskell{many}, similarly to
src_haskell{mconcat}, commonly occur in functions handling
src_haskell{Alternative}s and can have different definitions varying
in performance for different types.
The most common use of src_haskell{Alternative} type class is
parser combinators (\cref{sec:parser-combinators}) where
src_haskell{some} and src_haskell{many} coincide with =+= ("one or
more") and =*= ("zero or more", Kleene star) operators from regular
expressions/EBNF.
Before the introduction of src_haskell{Alternative} that role was
played by now deprecated src_haskell{MonadPlus} class, currently
defined in src_haskell{Control.Monad} of =base= as follows
#+BEGIN_SRC haskell :tangle tng-main.hs
class (Alternative m, Monad m) => MonadPlus m where
mzero :: m a
mzero = empty
mplus :: m a -> m a -> m a
mplus = (<|>)
#+END_SRC
We shall give example instance and usage of src_haskell{Alternative}
in \cref{sec:parser-combinators}.
** Purely src_haskell{Monad}ic
This subsection describes algebraic structures that involve
src_haskell{Monad} type class and its instances.
*** src_haskell{Monad} definition
@@tex:\label{sec:monad}@@
src_haskell{GHC.Base} from =base=~\cite{Hackage:base4900} defines
src_haskell{Monad} in the following way using the original (i.e. not
src_haskell{Pointed}) hierarchy (also, at the time of writing =base=
uses a bit uglier definition which is discussed in
\cref{sec:monad-fail})
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
infixl 1 >>=
class Applicative m => Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
#+END_SRC
\noindent and wants its instances to satisfy the following equations
known as "src_haskell{Monad} laws"
#+BEGIN_SRC haskell-spec
-- `return` is left identity for `(>>=)`
return a >>= f == f a
-- `return` is right identity for `(>>=)`
f >>= return == f
-- `(>>=)` is associative
(f >>= g) >>= h == f >>= (\x -> g x >>= h)
#+END_SRC
Note that this definition also expects the following additional
"unspoken laws" from its parent structures (see \cref{sec:boilerplate}
for definitions of src_haskell{liftM} and src_haskell{ap}).
#+BEGIN_SRC haskell-spec
fmap == liftM
pure == return
(<*>) == ap
#+END_SRC
Moreover, we feel that the name "return" itself is an unfortunate
accident since src_haskell{return} only injects pure values into
src_haskell{m} and does not "return" anywhere. We shall avoid that
problem and simplify the above equations by redefining
src_haskell{Monad} using src_haskell{Pointed} hierarchy instead
#+BEGIN_SRC haskell :tangle tng-main.hs
infixl 1 >>=
class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b
-- for backward-compatibility
return :: Monad m => a -> m a
return = pure
#+END_SRC
#+BEGIN_remark
@@tex:\label{rem:monad-as-app}@@
Note that while src_haskell{Applicative} is too weak to express
/generalized functions/ (\cref{rem:applicative-as-app}),
src_haskell{Monad}, in some sense, is too strong since
src_haskell{(>>=)} combines function composition (the whole type) with
lambda introduction (the type of the second argument). This might be
easier to see with the definition given in \cref{sec:monad-fish}.
What is the "just right" structure for representing a /generalized
function/ is a matter of debate: some would state "an
src_haskell{Arrow}!"~\cite{hughes-arrows-00}, others "a (Cartesian
Closed) src_haskell{Category}!"~\cite{Elliott:2017:CTC}, yet others
might disagree with both.
#+END_remark
A very common combinator used with src_haskell{Monad}s bears a name of
src_haskell{(>>)} and can be defined as
#+BEGIN_SRC haskell :tangle tng-main.hs
(>>) :: Monad m => m a -> m b -> m b
a >> b = a >>= const b
-- a >>= \_ -> b
#+END_SRC
The following subsections will provide many example instances.
*** src_haskell{MonadFish}
@@tex:\label{sec:monad-fish}@@
A somewhat lesser known but equivalent way to define
src_haskell{Monad} is to define src_haskell{(>>=)} in "fish" form as
follows
#+BEGIN_SRC haskell :tangle tng-main.hs
infixl 1 >=>
class Applicative m => MonadFish m where
(>=>) :: (a -> m b) -> (b -> m c) -> (a -> m c)
#+END_SRC
This way src_haskell{Monad} laws become src_haskell{Monoid} laws
#+BEGIN_SRC haskell-spec
-- `pure` is left identity for `(>=>)`
pure >=> f == f
-- `pure` is right identity for `(>=>)`
f >=> pure == f
-- `(>=>)` is associative
(f >=> g) >=> h == f >=> (g >=> h)
#+END_SRC
Both definitions of src_haskell{Monad} are known to be equivalent in
the folklore, but we could not find a reference with a simple proof of
that fact, hence we shall give one ourselves.
#+BEGIN_lemma
src_haskell{(f >=> g) . h == (f . h) >=> g}
#+END_lemma
#+BEGIN_proof
For pure values src_haskell{(>=>)} is a composition with flipped order
of arguments src_haskell{(.)}
#+BEGIN_SRC haskell :tangle tng-main.hs
instance MonadFish Identity where
f >=> g = g . runIdentity . f
#+END_SRC
In other words, src_haskell{f >=> g == g . f}, which gives the
following
#+BEGIN_SRC haskell-spec
(f >=> g) . h == h >=> (f >=> g)
== (h >=> pure) >=> (f >=> g)
== ((h >=> pure) >=> f) >=> g
== (h >=> f) >=> g
== (f . h) >=> g
#+END_SRC
\noindent which, with some abuse of notation (src_haskell{(>=>)} is
not heterogeneous, the above lifts pure values into src_haskell{m}
with src_haskell{pure}), can be written simply as
#+BEGIN_SRC haskell-spec
(f >=> g) . h == h >=> (f >=> g)
== (h >=> f) >=> g
== (f . h) >=> g
#+END_SRC
#+END_proof
#+BEGIN_lemma
src_haskell{Monad} and src_haskell{MonadFish} define the same structure.
#+END_lemma
#+BEGIN_proof
The cross-definitions:
#+BEGIN_SRC haskell :tangle tng-main.hs
instance (Applicative m, Monad m) => MonadFish m where
f >=> g = \a -> (f a) >>= g -- (1)
instance {-# OVERLAPPABLE #-}
(Applicative m, MonadFish m) => Monad m where
ma >>= f = (id >=> f) ma -- (2)
#+END_SRC
- (1) implies (2):
#+BEGIN_SRC haskell-spec
ma >>= f == (id >=> f) ma
== (\a -> id a >>= f) ma
== ma >>= f
#+END_SRC
- (2) implies (1):
#+BEGIN_SRC haskell-spec
f >=> g == \a -> (f a) >>= g
== \a -> (id >=> g) (f a)
== (id >=> g) . f
== (id . f) >=> g
== f >=> g
#+END_SRC
#+END_proof
*** src_haskell{Monad}'s fail and src_haskell{MonadFail}
@@tex:\label{sec:monad-fail}@@
Section~\ref{sec:monad} did not give the complete definition of
src_haskell{Monad} as is defined in the current version of
=base=~\cite{Hackage:base4900}. Current src_haskell{GHC.Base} module
defines src_haskell{Monad} in the following way using the original
(not src_haskell{Pointed}) hierarchy
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
infixl 1 >>=
class Applicative m => Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
fail :: String -> m a
fail s = error s
#+END_SRC
Note the definition of the src_haskell{fail} operation. That function
is invoked by the compiler on pattern match failures in
src_haskell{do}-expressions (see \cref{sec:non-exhaustive} for
examples, see \cref{sec:error-undefined} for the definition of
src_haskell{error}), but it can also be called explicitly by the
programmer in any context where the type permits to do so.
The presence of src_haskell{fail} in src_haskell{Monad} class is,
clearly[fn::It involves an error handling mechanism that is more
complicated than the thing itself. It creates semantic discrepancies
(e.g. src_haskell{Maybe} is not equivalent to src_haskell{Either ()},
see \cref{sec:either}).], a hack. There is an ongoing effort (aka
"src_haskell{MonadFail} proposal", "MFP") to move this function from
src_haskell{Monad} to its own type class defined as follows (in both
hierarchies)
#+BEGIN_SRC haskell :tangle tng-main.hs
class Monad m => MonadFail m where
fail :: String -> m a
fail s = error s
#+END_SRC
As of writing of this article the new class is available from
src_haskell{Control.Monad.Fail}, but src_haskell{fail} from the
original src_haskell{Monad} is not even deprecated yet. We shall use
src_haskell{MonadFail} instead of the original src_haskell{fail} in
our hierarchy for simplicity.
*** src_haskell{Identity} monad
@@tex:\label{sec:identity-monad}@@
We can define the following src_haskell{Monad} and
src_haskell{MonadFail} instances for the src_haskell{Identity}
src_haskell{Functor}
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Monad Identity where
(Identity x) >>= f = f x
instance MonadFail Identity where
-- default implementation
#+END_SRC
\noindent despite this instance it is still usually referenced as
"src_haskell{Identity} src_haskell{Functor}" even though it is also
an src_haskell{Applicative} and a src_haskell{Monad}.
*** src_haskell{Maybe} monad
@@tex:\label{sec:maybe}@@
The simplest form of src_haskell{Monad}ic error handling (that is, not
just "error ignoring") can be done with src_haskell{Maybe} data type
and its src_haskell{Monad} instance defined in src_haskell{Data.Maybe}
of =base=~\cite{Hackage:base4900} equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
data Maybe a = Nothing | Just a
instance Pointed Maybe where
pure = Just
instance Monad Maybe where
(Just x) >>= k = k x
Nothing >>= _ = Nothing
instance MonadFail Maybe where
-- custom `fail`
fail _ = Nothing
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
deriving instance Eq a => Eq (Maybe a)
deriving instance Show a => Show (Maybe a)
#+END_SRC
The src_haskell{pure} operator simply injects a given value under
src_haskell{Just} constructor, while the definition of
src_haskell{(>>=)} ensures that
- injected values are transparently propagated further down the
computation path,
- computation stops as soon as the first src_haskell{Nothing}
gets emitted.
In other words, src_haskell{Maybe} src_haskell{Monad} is
src_haskell{Identity} src_haskell{Monad} that can stop its computation
on request. A couple of examples follow
#+BEGIN_SRC haskell :tangle tng-main.hs
maybeTest1 :: Maybe Int
maybeTest1 = do
x <- Just 1
pure x
maybeTest2 :: Maybe Int
maybeTest2 = do
x <- Just 1
pure x
Nothing
Just 2
maybeTest = maybeTest1 == Just 1
&& maybeTest2 == Nothing
#+END_SRC
*** src_haskell{Either} monad
@@tex:\label{sec:either}@@
src_haskell{Either} data type is defined in src_haskell{Data.Either} of
=base=~\cite{Hackage:base4900} equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
data Either a b = Left a | Right b
instance Pointed (Either e) where
pure = Right
instance Monad (Either e) where
Left l >>= _ = Left l
Right r >>= k = k r
instance MonadFail (Either e)
-- default `fail`
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
deriving instance (Eq a, Eq b) => Eq (Either a b)
deriving instance (Show a, Show b) => Show (Either a b)
#+END_SRC
src_haskell{Either} is a computation that can stop and report a given
value (the argument of src_haskell{Left}) when falling out of
src_haskell{Identity} execution. The intended use is similar to
src_haskell{Maybe}
#+BEGIN_SRC haskell :tangle tng-main.hs
eitherTest1 :: Either String Int
eitherTest1 = do
x <- Right 1
pure x
eitherTest2 :: Either String Int
eitherTest2 = do
x <- Right 1
pure x
Left "oops"
Right 2
eitherTest = eitherTest1 == Right 1
&& eitherTest2 == Left "oops"
#+END_SRC
Purely by its data type definition src_haskell{Maybe a} is isomorphic
to src_haskell{Either () a} (where src_haskell{()} is Haskell's name
for the ML's src_ocaml{unit} type and type-theoretic "top" type), but
their src_haskell{Monad} instances (in the original hierarchy,
src_haskell{MonadFail} in our hierarchy) differ: src_haskell{Maybe}
has non-default src_haskell{fail}, while src_haskell{Either} does not.
This produces some observable differences discussed in
\cref{sec:non-exhaustive}.
** An intermission on src_haskell{Monad}ic boilerplate
@@tex:\label{sec:boilerplate}@@
Haskell does not support default definitions for functions in
superclasses that use definitions given in subclasses. That is,
Haskell has no syntax to define src_haskell{Functor}
and src_haskell{Applicative} defaults from src_haskell{Monad}
instance of the same type.
Which is why to compile the code above we have to borrow a couple of
functions from src_haskell{Control.Monad} of =base=
#+BEGIN_SRC haskell :tangle tng-main.hs
liftM :: (Monad m)
=> (a -> b) -> m a -> m b
liftM f ma = ma >>= pure . f
ap :: (Monad m)
=> m (a -> b) -> m a -> m b
ap mf ma = mf >>= \f -> liftM f ma
#+END_SRC
\noindent and use them to define
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Functor Maybe where
fmap = liftM
instance Applicative Maybe where
(<*>) = ap
#+END_SRC
\noindent and analogously for src_haskell{Either}. For all the
listings that follow we shall silently hide this type of boiler-plate
code from the paper version where appropriate (it can still be
observed in the Literate Haskell version).
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor (Either e) where
fmap = liftM
instance Applicative (Either e) where
(<*>) = ap
#+END_SRC
** src_haskell{MonadTrans}formers
The problem with src_haskell{Monad}s is that they, in general, do not
compose. src_haskell{Monad} transformers~\cite{Liang:1995:MTM} provide
a systematic way to define structures that represent "a
src_haskell{Monad} with a hole" that allow computations from an inner
src_haskell{Monad} src_haskell{m} to be src_haskell{lift}ed through a
hole in an outer src_haskell{Monad (t m)} (src_haskell{t} transforms
monad src_haskell{m}, hence "monad transformer"). The main type class
is defined in src_haskell{Control.Monad.Trans.Class} module of
=transformers=~\cite{Hackage:transformers0520} package as follows
#+BEGIN_SRC haskell :tangle tng-main.hs
class MonadTrans t where
lift :: (Monad m) => m a -> t m a
#+END_SRC
Haskell type class system is not flexible enough to encode the
requirement that src_haskell{t m} needs to be a src_haskell{Monad} in
a single definition, so it has to be encoded in every instance by
using the following instance schema
#+BEGIN_SRC haskell-spec
instance Monad m => Monad (t m) where
-- ...
#+END_SRC
Different src_haskell{MonadTrans}formers (src_haskell{t1},
src_haskell{t2} \dots src_haskell{tn}) can then be composed with an
arbitrary src_haskell{Monad} src_haskell{m} (usually called "/the/
inner src_haskell{Monad}") using the following scheme
#+BEGIN_SRC haskell-spec
newtype comp m a = t1 (t2 (.. (tn (m a))))
#+END_SRC
\noindent and the whole src_haskell{comp}osed stack would get a
src_haskell{Monad} instance inferred for it. Popular choices for the
inner src_haskell{Monad} src_haskell{m} include
src_haskell{Identity} src_haskell{Functor} and src_haskell{IO}
src_haskell{Monad} (see \cref{sec:imprecise}).
In short, src_haskell{MonadTrans}formers are, pretty much, composable
src_haskell{Monad}ic structures. The following subsections will
provide many example instances. For an in-depth tutorial readers
are referred to \cite{Jones:1995:FPO} and~\cite{Liang:1995:MTM}.
*** src_haskell{Identity}
@@tex:\label{sec:identity-monadtrans}@@
The simplest src_haskell{MonadTrans}former is src_haskell{IdentityT}
defined in src_haskell{Control.Monad.Trans.Identity} of
=transformers=~\cite{Hackage:transformers0520} package equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype IdentityT m a = IdentityT
{ runIdentityT :: m a }
instance MonadTrans IdentityT where
lift = IdentityT
instance Monad m
=> Pointed (IdentityT m) where
pure = lift . pure
instance Monad m
=> Monad (IdentityT m) where
x >>= f = IdentityT $ do
v <- runIdentityT x
runIdentityT (f v)
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monad m => Functor (IdentityT m) where
fmap = liftM
instance Monad m => Applicative (IdentityT m) where
(<*>) = ap
#+END_SRC
#+BEGIN_remark
@@tex:\label{rem:identity-transformer}@@
Note that src_haskell{IdentityT} src_haskell{MonadTrans}former is
different from src_haskell{Identity} src_haskell{Monad} and cannot be
redefined as simply
#+BEGIN_SRC haskell :tangle tng-main.hs
type IdentityT' m a = Identity (m a)
#+END_SRC
\noindent (even though the data type definition matches exactly)
because src_haskell{IdentityT} "inherits" src_haskell{Monad}
implementation from its argument src_haskell{m} while
src_haskell{Identity} provides its own. I.e. src_haskell{IdentityT}
is an identity on src_haskell{MonadTrans}formers while
src_haskell{Identity} is an identity on types.
In particular, for src_haskell{Identity (Maybe a)}
#+BEGIN_SRC haskell-spec
pure == Identity
#+END_SRC
\noindent while for src_haskell{IdentityT Maybe a}
#+BEGIN_SRC haskell-spec
pure == IdentityT . pure == IdentityT . Just
#+END_SRC
#+END_remark
*** src_haskell{Maybe}
Transformer version of src_haskell{Maybe} called src_haskell{MaybeT}
is defined in src_haskell{Control.Monad.Trans.Maybe} from
=transformers=~\cite{Hackage:transformers0520} package equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype MaybeT m a = MaybeT
{ runMaybeT :: m (Maybe a) }
instance MonadTrans MaybeT where
lift = MaybeT . liftM Just
instance Monad m
=> Pointed (MaybeT m) where
pure = lift . pure
instance Monad m
=> Monad (MaybeT m) where
x >>= f = MaybeT $ do
v <- runMaybeT x
case v of
Nothing -> pure Nothing
Just y -> runMaybeT (f y)
instance MonadFail m
=> MonadFail (MaybeT m) where
fail _ = MaybeT (pure Nothing)
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monad m => Functor (MaybeT m) where
fmap = liftM
instance Monad m => Applicative (MaybeT m) where
(<*>) = ap
#+END_SRC
*** src_haskell{Except}
@@tex:\label{sec:either-monadtrans}@@
Transformer version of src_haskell{Either} for historical reasons
bears a name of src_haskell{ExceptT} and is defined in
src_haskell{Control.Monad.Trans.Except} from
=transformers=~\cite{Hackage:transformers0520} package equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype ExceptT e m a
= ExceptT { runExceptT
:: m (Either e a) }
instance MonadTrans (ExceptT e) where
lift = ExceptT . liftM Right
instance Pointed m
=> Pointed (ExceptT e m) where
pure a = ExceptT $ pure (Right a)
instance Monad m
=> Monad (ExceptT e m) where
m >>= k = ExceptT $ do
a <- runExceptT m
case a of
Left e -> pure (Left e)
Right x -> runExceptT (k x)
instance MonadFail m
=> MonadFail (ExceptT e m) where
fail = ExceptT . fail
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monad m => Functor (ExceptT e m) where
fmap = liftM
instance Monad m => Applicative (ExceptT e m) where
(<*>) = ap
#+END_SRC
The main attraction of src_haskell{ExceptT} for the purposes of this
article is the fact that it provides its own non-imprecise
non-dynamic-dispatching src_haskell{throw} and src_haskell{catch}
operators defined as
#+BEGIN_SRC haskell :tangle tng-main.hs
throwE :: (Monad m) => e -> ExceptT e m a
throwE = ExceptT . pure . Left
catchE :: (Monad m) =>
ExceptT e m a
-> (e -> ExceptT f m a)
-> ExceptT f m a
m `catchE` h = ExceptT $ do
a <- runExceptT m
case a of
Left l -> runExceptT (h l)
Right r -> pure (Right r)
#+END_SRC
There also exists deprecated src_haskell{ErrorT} (defined in
src_haskell{Control.Monad.Trans.Error} from =transformers= package)
which at the time of writing has exactly the same definition as
src_haskell{ExceptT}
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype ErrorT e m a
= ErrorT { runErrorT
:: m (Either e a) }
#+END_SRC
\noindent but its instances require type class
src_haskell{Exception} (see \cref{sec:exception}) from its argument
src_haskell{e}. Older versions of =transformers= package made this
requirement in the definition of src_haskell{ErrorT}
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_SRC haskell-spec
newtype ErrorT e m a
= Exception e =>
ErrorT { runErrorT
:: m (Either e a) }
#+END_SRC
\noindent but that mechanism itself was deprecated awhile ago.
*** src_haskell{Reader} and src_haskell{State}
@@tex:\label{sec:reader-state-monadtrans}@@
While there seems to be no way to directly use src_haskell{Reader} and
src_haskell{State} src_haskell{Monad}s for error handling, these
structures are used in src_haskell{IO} src_haskell{Monad} of
\cref{sec:imprecise} and parser combinators of
\cref{sec:parser-combinators}. This seems to be as good place as any
to define them.
src_haskell{Reader} src_haskell{Monad} is defined in
src_haskell{Control.Monad.Trans.Reader} module of
=transformers=~\cite{Hackage:transformers0520} package equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
type Reader s = ReaderT s Identity
newtype ReaderT s m a = ReaderT { runReaderT :: s -> m a }
instance MonadTrans (ReaderT s) where
lift m = ReaderT $ \_ -> m
instance Pointed m => Pointed (ReaderT s m) where
pure a = ReaderT $ \_ -> pure a
instance Monad m => Monad (ReaderT s m) where
m >>= k = ReaderT $ \s -> do
a <- runReaderT m s
runReaderT (k a) s
instance MonadFail m => MonadFail (ReaderT s m) where
fail str = ReaderT $ \_ -> fail str
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monad m => Functor (ReaderT s m) where
fmap = liftM
instance Monad m => Applicative (ReaderT s m) where
(<*>) = ap
#+END_SRC
Meanwhile, src_haskell{State} src_haskell{Monad} is defined in
src_haskell{Control.Monad.Trans.State.Lazy} and
src_haskell{Control.Monad.Trans.State.Strict} modules (the difference
between them does not matter for the purposes of this article, so we
shall ignore it) from =transformers=~\cite{Hackage:transformers0520}
package equivalently to
#+BEGIN_SRC haskell :tangle tng-main.hs
type State s = StateT s Identity
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
instance MonadTrans (StateT s) where
lift m = StateT $ \s -> do
a <- m
pure (a, s)
instance Pointed m => Pointed (StateT s m) where
pure a = StateT $ \s -> pure (a, s)
instance Monad m => Monad (StateT s m) where
m >>= k = StateT $ \s -> do
(a, s') <- runStateT m s
runStateT (k a) s'
instance MonadFail m => MonadFail (StateT s m) where
fail str = StateT $ \_ -> fail str
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monad m => Functor (StateT s m) where
fmap = liftM
instance Monad m => Applicative (StateT s m) where
(<*>) = ap
#+END_SRC
Both structures provide src_haskell{Monad}ic structures that handle
state. src_haskell{ReaderT} simply applies variable src_haskell{s}
throughout its whole computation via its src_haskell{(>>=)} operator
thus supplying computations with a /context/ (i.e. read-only /state/).
Meanwhile, src_haskell{StateT} chains its src_haskell{s} between
computations, thus providing computations with a (read-write) /state/.
** Imprecise exceptions
@@tex:\label{sec:imprecise}@@
As we mentioned in the introduction, GHC implements /imprecise
exceptions/ mechanism proposed in \cite{PeytonJones:1999:SIE}. Such
exceptions look superficially similar to those of C++/Java/Python/etc
but differ in two important aspects.
Firstly, GHC imprecise exceptions in pure computations are completely
imprecise. That is, evaluation of src_haskell{(a `op` b)} with
src_haskell{a} raising src_haskell{e} and src_haskell{b} raising
src_haskell{f} (and assuming src_haskell{op} can evaluate either
argument first) can raise either or even both (on different
evaluations) of src_haskell{e} and src_haskell{f}. Haskell is not the
only language that does this, C++, for instance, defines /sequence
points/ that serve the same purpose~\cite{CFAQ:SeqPoints}. However, in
GHC the order in which exception are raised is limited only by data
dependencies, while C++'s sequence points add some more ordering on
top.
Secondly, the C++/Java/Python exceptions have dynamic dispatch
builtin, while GHC's dynamically dispatched exceptions are implemented
as a library on top of statically dispatched exceptions. To be more
specific
- on the base level GHC runtime defines src_haskell{raise#} and
src_haskell{catch#} operations for which src_haskell{raise#}
"simply"[fn::@@tex:\label{fn:simply}@@We put "simply" and "just" into
quotes since unwinding of the stack must unwind into the lexically
correct handler which is nontrivial in a lazy language like Haskell
where thunks can be evaluated in an environment different from the
one they were created in. In short, thunks must capture exception
handlers as well as variables.] unwinds the stack to the closest
src_haskell{catch#} (i.e. src_haskell{raise#} is
"just"\cref{fn:simply} a src_assembly{GOTO}; src_haskell{cast}ing,
re-src_haskell{raise}ing, src_haskell{finally}, etc are left for the
libraries to implement and are not builtins),
- on top of that GHC libraries then provide dynamically dispatched
exceptions by src_haskell{cast}ing elements of src_haskell{Typeable}
types from/to src_haskell{SomeException} existential
type~\cite{Marlow:2006:EDH}.
In the following subsections we shall discuss the details of the actual
implementation.
*** src_haskell{IO}
@@tex:\label{sec:io}@@
GHC defines the mystical src_haskell{IO} src_haskell{Monad} in
src_haskell{GHC.Types} (the types) and src_haskell{GHC.Base} (the
instances), pretty much, as a src_haskell{State} src_haskell{Monad}
(see \cref{sec:reader-state-monadtrans}) on src_haskell{State# RealWorld}
(definitions of both of which are beyond the scope of this article)
#+BEGIN_SRC haskell :tangle tng-main.hs
type IO# a = State# RealWorld
-> (# State# RealWorld, a #)
newtype IO a = IO { runIO :: IO# a }
instance Pointed IO where
pure a = IO $ \s -> (# s, a #)
instance Monad IO where
m >>= f = IO $ \s -> case runIO m s of
(# s', a #) -> runIO (f a) s'
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor IO where
fmap = liftM
instance Applicative IO where
(<*>) = ap
#+END_SRC
The src_haskell{IO#} definition given above is not actually in GHC but
without it all of the definitions below become unreadable. We also
renamed src_haskell{unIO} to src_haskell{runIO} for uniformity with
src_haskell{State}. Note however, that we did not swap the elements of
the result tuple of src_haskell{IO#} to match those of
src_haskell{State} since that would make it incompatible with GHC
runtime we reuse in Literate Haskell version.
#+BEGIN_remark
@@tex:\label{rem:io-caveats}@@
Note that src_haskell{IO} is not a proper src_haskell{Monad} since it
cannot satisfy the laws simply for the fact that
src_haskell{RealWorld} cannot have an equality.[fn::Although
src_haskell{IO} can be reformulated as a free src_haskell{Monad} made
of "requests to the interpreter" and continuations if one is willing
to forget about the internal structure of the
src_haskell{RealWorld}~\cite{Kmett:2011:FMFL}.]
In this article, however, for the purposes of formal arguments
involving src_haskell{IO} we shall treat src_haskell{IO} as if it was
just a src_haskell{State} over some state type with some simple
denotational semantics (although, possibly unknown value). This, of
course, immediately disqualifies our proofs for src_haskell{IO} from
using non-determinism, hence, for instance, we will not be able to prove
things about imprecise exceptions or threads.
The alternative would be to split every lemma and theorem mentioning
src_haskell{IO} into two: one for a src_haskell{RawMonad}
(src_haskell{Monad} without laws) for cases mentioning
src_haskell{IO}, and one for src_haskell{Monad} for all other cases.
This would make a very little practical sense for this article since
we will not attempt proofs involving non-determinism anyway.
#+END_remark
*** src_haskell{raise#} and src_haskell{catch#}
@@tex:\label{sec:raise-catch}@@
Primitive src_haskell{raise#} and src_haskell{catch#} operations are
"defined" (those, of course, are just stubs to be replaced by
references to the actual implementations in GHC runtime) in
src_haskell{GHC.Prim} module like follows
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
raise# :: a -> b
raise# = raise#
catch# :: IO# a -> (b -> IO# a)
-> IO# a
catch# = catch#
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Adapting GHC.Prim functions for use in this file
{-# NOINLINE raise# #-}
raise# :: a -> b
raise# a = (GP.raise#) a
{-# NOINLINE catch# #-}
catch# :: IO# a -> (b -> IO# a)
-> IO# a
catch# a b c = (GP.catch#) a b c
#+END_SRC
Evaluating src_haskell{raise#} "simply"\cref{fn:simply} unwinds
computation stack to the point of the closet src_haskell{catch#} with
the appropriate type and applies raised value to the second argument
of the latter. Note, however, that while the type of
src_haskell{raise#} permits its use anywhere in the program,
src_haskell{catch#} is sandboxed to src_haskell{IO#} on the lowest
observable level and GHC provides no "src_haskell{unsafeCatch}". This
allows GHC to perform many useful optimizations that influence
evaluation order without exposing pure computations to
non-determinism.
*** src_haskell{Typeable}
@@tex:\label{sec:typeable}@@
GHC implements dynamic casting with src_haskell{Typeable} type class.
The details of its actual implementation are beyond the scope of this
article. For our purposes it suffices to say that it is a type class
of types that have type representations that can be compared at
runtime
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
class Typeable a where
-- magic beyond the scope of this article
#+END_SRC
\noindent and it provides a src_haskell{cast} operation with the
following type signature that shows that it compares said
representations of types of its argument and result and either
returns its argument value wrapped in src_haskell{Just} constructor
when the types match or src_haskell{Nothing} else
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
cast :: forall a b
. (Typeable a, Typeable b)
=> a -> Maybe b
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs :exports none
-- Beyond the scope of this article
cast = cast
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Adapting Data.Typeable.cast for our Maybe
cast :: forall a b
. (Typeable a, Typeable b)
=> a -> Maybe b
cast g = case T.cast g of
P.Nothing -> Nothing
P.Just a -> Just a
#+END_SRC
Interested readers should inspect the source code of
src_haskell{Data.Typeable} module of =base=~\cite{Hackage:base4900}.
*** src_haskell{Exception}
@@tex:\label{sec:exception}@@
On top of src_haskell{Typeable} in src_haskell{GHC.Exception} module
of =base=~\cite{Hackage:base4900} GHC provides the
src_haskell{Exception} type class that casts values to and from
src_haskell{SomeException} existential type (the following syntactic
src_haskell{forall} is type-theoretic src_haskell{exists}, historic
reasons)
#+BEGIN_SRC haskell :tangle tng-main.hs
data SomeException = forall e. Exception e
=> SomeException e
class (Typeable e, Show e) => Exception e where
toException :: e -> SomeException
fromException :: SomeException-> Maybe e
toException = SomeException
fromException (SomeException e) = cast e
instance Show SomeException where
show (SomeException e) = show e
instance Exception SomeException where
toException = id
fromException x = Just x
#+END_SRC
*** src_haskell{throw} and src_haskell{catch}
\label{sec:throw-catch}
Finally, src_haskell{throw} and src_haskell{catch} operators defined
in src_haskell{GHC.Exception} module of =base=~\cite{Hackage:base4900}
use all of the above to implement dynamic dispatch of exceptions.
The src_haskell{throw} operator simply wraps given exception into
src_haskell{SomeException} and src_haskell{raise#}s
#+BEGIN_SRC haskell :tangle tng-main.hs
throw :: Exception e => e -> a
throw e = raise# (toException e)
#+END_SRC
The src_haskell{catchException} operator defined in
src_haskell{GHC.IO} does the actual dynamic dispatch
- it src_haskell{catch#}es an exception produced by its first argument
("computation"),
- tries to src_haskell{cast} it to a type expected by its second
argument ("handler") and either calls the latter on success, or
src_haskell{raise#}s again on failure.
#+BEGIN_SRC haskell :tangle tng-main.hs
catchException :: Exception e
=> IO a -> (e -> IO a)
-> IO a
catchException (IO io) handler
= IO $ catch# io handler'
where
handler' e = case fromException e of
Just f -> runIO (handler f)
Nothing -> raiseIO# e
#+END_SRC
The src_haskell{catch} operator simply calls
src_haskell{catchException} after forcing its first argument into a
thunk with src_haskell{lazy} operator (this wrapping is necessary to
prevent GHC from performing strictness analysis on the "computation"
to prevent its evaluation before the exception is even raised; this
fact can be ignored for the purposes of this article) which is yet
another special GHC runtime function (this time, extentionally equal
to its definition, i.e. identity).
#+BEGIN_SRC haskell :tangle tng-main.hs
lazy :: a -> a
lazy x = x
catch :: Exception e
=> IO a -> (e -> IO a)
-> IO a
catch act = catchException (lazy act)
#+END_SRC
That is, src_haskell{catch} is extentionally equal to
src_haskell{catchException}.
src_haskell{Control.Exception} module of =base= simply reexports
src_haskell{throw}, src_haskell{catch}, and src_haskell{Exception}
type class and implements a bunch of practically convenient
combinators using them.
We should also mention that older versions of =base= package had
another special src_haskell{catch} that handled only
src_haskell{IOError}s defined in src_haskell{Prelude} and
src_haskell{System.IO.Error} respectively. Those were deprecated in
2011 and as of writing of this article are completely gone from
current version of =base=. But they are are occasionally mentioned in
tutorials, usually in the context of "don't use src_haskell{catch}
from src_haskell{Prelude}, use the one from
src_haskell{Control.Exception}", nowadays the src_haskell{catch} from
src_haskell{Prelude} /is/ the src_haskell{catch} from
src_haskell{Control.Exception}.
# TODO(low): IOError is not highlighed above
*** src_haskell{error} and src_haskell{undefined}
@@tex:\label{sec:error-undefined}@@
src_haskell{error} and src_haskell{undefined} primitives are defined
in src_haskell{GHC.Err} of =base= as follows
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype ErrorCall = ErrorCall String
instance Exception ErrorCall where
error :: String -> a
error s = throw (ErrorCall s)
undefined :: forall a . a
undefined = error "Prelude.undefined"
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Show ErrorCall where
show _ = "error"
deriving instance Typeable ErrorCall
#+END_SRC
Actually, this implementation is taken from the older version of
=base=, modern version also implements call stack capture, which is
beyond the scope of this article. Interested readers are referred to
the source code of src_haskell{GHC.Err}.
** Precise src_haskell{raiseIO#} and src_haskell{throwIO}
Besides imprecise exceptions GHC's src_haskell{IO} also has operators
for precise exceptions a-la src_haskell{ExceptT} defined in
src_haskell{GHC.Prim} and src_haskell{GHC.Exception} as follows
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
raiseIO# :: a -> IO# b
raiseIO# = raiseIO#
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
{-# NOINLINE raiseIO# #-}
raiseIO# :: a -> IO# b
raiseIO# a b = (GP.raiseIO#) a b
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs
throwIO :: Exception e => e -> IO a
throwIO e = IO $ raiseIO# (toException e)
#+END_SRC
While src_haskell{throwIO} has a type that is an instance of
src_haskell{throw}, their semantics differ: src_haskell{throwIO}
produces src_haskell{Monad}ic actions while src_haskell{throw}
produces values. For example, both functions in the following example
will raise src_haskell{SomethingElse}, not src_haskell{ErrorCall}.
#+BEGIN_SRC haskell :tangle tng-main.hs
data SomethingElse = SomethingElse
instance Exception SomethingElse where
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Show SomethingElse where
show _ = "something"
deriving instance Typeable SomethingElse
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs
throwTest :: IO ()
throwTest = do
let x = throw (ErrorCall "lazy")
pure (Right x)
throwIO SomethingElse
throwTest' :: IO ()
throwTest' = do
let x = throw (ErrorCall "lazy")
pure x
throwIO SomethingElse
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- for ghci
evalIO (IO a) = GT.IO a
throwTestIO = evalIO throwTest
throwTestIO' = evalIO throwTest'
#+END_SRC
The src_haskell{catch} operator, however, can be reused for handling
both imprecise and precise exceptions.
#+BEGIN_remark
@@tex:\label{rem:io-two-kinds-of-exceptions}@@
In other words, we can say that src_haskell{IO} has two different
exception mechanisms (precise and imprecise exceptions) with a single
exception handling mechanism (src_haskell{catch}). (And this is pretty
weird.)
#+END_remark
** Non-exhaustive patterns
@@tex:\label{sec:non-exhaustive}@@
As a side note, non-exhaustive pattern matches (and
src_haskell{case}s) src_haskell{throw} src_haskell{PatternMatchFail}
exception, while the default src_haskell{fail} implementation calls
src_haskell{error} which src_haskell{throw}s src_haskell{ErrorCall}.
#+BEGIN_SRC haskell :tangle tng-patterns.hs
{-# LANGUAGE ScopedTypeVariables #-}
import Control.Exception
check t =
(evaluate t >> print "ok")
`catch`
(\(e :: PatternMatchFail)
-> print "throws PatternMatchFail")
`catch`
(\(e :: ErrorCall)
-> print "throws ErrorCall")
patFail 1 x = case x of 0 -> 1
fail1 = patFail 1 1
fail2 = patFail 2 2
maybeDont = do { 1 <- Just 1 ; return 2 }
maybeFail = do { 0 <- Just 1 ; return 2 }
eithrDont = do { 1 <- Right 1 ; return 2 }
eithrFail = do { 0 <- Right 1 ; return 2 }
testPatterns = do
check fail1 -- throws PatternMatchFail
check fail2 -- throws PatternMatchFail
check maybeDont -- ok
check maybeFail -- ok (`Nothing`)
check eithrDont -- ok
check eithrFail -- throws ErrorCall
#+END_SRC
** src_haskell{Monad}ic generalizations
@@tex:\label{sec:monadic-generalizations}@@
In previous subsections we have seen a plethora of slightly different
error handling structures with different src_haskell{throw} and
src_haskell{catch} operators. In this subsection we shall describe
several Hackage packages that provide structures that try to unify
this algebraic zoo.
*** src_haskell{MonadError}
@@tex:\label{sec:monad-error}@@
src_haskell{MonadError} class (src_haskell{Control.Monad.Error.Class}
from =mtl=~\cite{Hackage:mtl221} package) is defined as
#+BEGIN_SRC haskell :tangle tng-main.hs
class (Monad m) => MonadError e m
| m -> e where
throwError :: e -> m a
catchError :: m a
-> (e -> m a) -> m a
#+END_SRC
This structure simply generalizes src_haskell{ExceptT}
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Monad m => MonadError e (ExceptT e m) where
throwError = throwE
catchError = catchE
#+END_SRC
\noindent in a way that is transitive over many other
src_haskell{MonadTrans}formers, for instance
#+BEGIN_SRC haskell :tangle tng-main.hs
-- (these require UndecidableInstances GHC extension, however)
instance MonadError e m => MonadError e (IdentityT m) where
throwError = lift . throwError
catchError a h = IdentityT $ catchError (runIdentityT a) (runIdentityT . h)
instance MonadError e m => MonadError e (MaybeT m) where
throwError = lift . throwError
catchError a h = MaybeT $ catchError (runMaybeT a) (runMaybeT . h)
#+END_SRC
*** src_haskell{MonadThrow} and src_haskell{MonadCatch}
@@tex:\label{sec:monad-catch}@@
src_haskell{MonadThrow} and src_haskell{MonadCatch} classes
(src_haskell{Control.Monad.Catch} from
=exceptions=~\cite{Hackage:exceptions083}) are defined as[fn::Except
for the fact that src_haskell{MonadCatch} from =exceptions= names its
operator src_haskell{catch}, not src_haskell{catchM}, we renamed it
for uniformity and so that it would not be confused with the operator
from src_haskell{Control.Exception}.]
#+BEGIN_SRC haskell :tangle tng-main.hs
class Monad m => MonadThrow m where
throwM :: Exception e => e -> m a
class MonadThrow m => MonadCatch m where
catchM :: Exception e
=> m a -> (e -> m a) -> m a
#+END_SRC
These two structures, too, generalizes src_haskell{ExceptT}
#+BEGIN_SRC haskell :tangle tng-main.hs
instance MonadThrow m => MonadThrow (ExceptT e m) where
throwM = lift . throwM
instance MonadCatch m => MonadCatch (ExceptT e m) where
catchM x f = ExceptT $ catchM (runExceptT x) (runExceptT . f)
#+END_SRC
\noindent and they, too, are transitive over common
src_haskell{MonadTrans}formers
#+BEGIN_SRC haskell :tangle tng-main.hs
-- (this time without UndecidableInstances)
instance MonadThrow m => MonadThrow (IdentityT m) where
throwM = lift . throwM
instance MonadCatch m => MonadCatch (IdentityT m) where
catchM x f = IdentityT $ catchM (runIdentityT x) (runIdentityT . f)
instance MonadThrow m => MonadThrow (MaybeT m) where
throwM = lift . throwM
instance MonadCatch m => MonadCatch (MaybeT m) where
catchM x f = MaybeT $ catchM (runMaybeT x) (runMaybeT . f)
#+END_SRC
\noindent but they constrain their argument src_haskell{e} to the
src_haskell{Exception} type class, and they also generalize the
imprecise exceptions
#+BEGIN_SRC haskell :tangle tng-main.hs
instance MonadThrow IO where
throwM = throw
instance MonadCatch IO where
catchM = catch
#+END_SRC
The latter fact complicates their use somewhat since one can not be
sure about the dynamic-dispatch part of the semantics without actually
looking at the definitions for a particular instance.
* Not a Tutorial: Side B
@@tex:\label{sec:tutorial:non-basic}@@
This section, logically, is a continuation of
\cref{sec:tutorial:basic}. However, in contrast to that section this
section discusses non-basic structures that are of particular
importance to the rest of the article. While this section does not
introduce any non-trivial novel ideas, some perspectives on well-known
ideas seem to be novel.
** src_haskell{Cont}inuations
@@tex:\label{sec:continuations}@@
When speaking of "continuations" people usually mean one or more of
the three related aspects explained in this subsection.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Just a bunch of stubs for examples below
something = something
result1 = undefined
result2 = undefined
data Result a b = Result1 a | Result2 b
bar1 = undefined
bar2 = undefined
computation = undefined
isError = undefined
handle = undefined
#+END_SRC
*** Continuation-Passing Style
Any (sub-)program can be rewritten into Continuation-Passing Style
(CPS)~\cite{Reynolds:1993:DC,appel-92} by adding a number of
additional /continuation/ arguments to every function and tail-calling
into those arguments with the results-to-be at every return point
instead of just returning said results.
For instance, the following pseudo-Haskell program
#+BEGIN_SRC haskell :tangle tng-main.hs
foo =
if something
then Result1 result1
else Result2 result2
bar = case foo of
Result1 a -> bar1 a
Result2 b -> bar2 b
#+END_SRC
\noindent can be transformed into (here we CPS-ignore
src_haskell{something} and the src_haskell{if} for illustrative
purposes)
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_SRC haskell :tangle tng-main.hs
fooCPS cont1 cont2 =
if something
then cont1 result1
else cont2 result2
barCPS = fooCPS bar1 bar2
#+END_SRC
In conventional modern low-level imperative terms this transformation
requires all functions to receive their return addresses as explicit
parameters instead of
src_assembly{pop}ing them from the bottom of their stack frame.
The latter, of course, means that we can treat "/normal/" programs (in
which all functions have a single return address) as a degenerate case
of programs written in "/implicit-CPS/" (in fact, src_haskell{Cont}
src_haskell{Monad} of \cref{sec:cont} is exactly such an
"/implicit-CPS/") --- a syntactic variant of CPS in which
- every function has an implicit argument that specifies a default
return address (which is set to the next instruction following a
corresponding function call by default)
- that can be reached from the body of the function by tail-calling a
special symbol that src_assembly{jmp}s to the implicitly given
address.
Finally, one can even imagine a computer with a "/CPS-ISA/" (i.e. an
ISA where each instruction explicitly specifies its own return
address) in which case all programs for such a computer would have to
be translated into an explicit CPS form to be executed. In fact, drum
memory-based computers like IBM 650 had exactly such an ISA. From the
point of view of an IBM 650 programmer modern conventional CPUs simply
convert their non-CPS OPcodes into their CPS forms on the fly, thus
applying CPS-transform to any given program on the fly.
Returning to the pseudo-Haskell listing above, note that programs
written in CPS
- introduce a linear order on their computations, hence they are not
particularly good for parallel execution,
- consume somewhat more memory in comparison to their "/normal/"
representations (as they have to handle more explicit addresses),
- can have poorer performance on modern conventional CPUs (since said
CPUs split their branch predictors into "jump" and "call" units and
the latter unit rests completely unused by CPS programs),
- are harder to understand.
However, the advantage of the CPS form is that it allows elimination
of duplicate computations. For instance, in the example above
src_haskell{foo} produces different results depending on the value of
src_haskell{something} and src_haskell{bar} has to duplicate that
choice (but not the computation of src_haskell{something}) again by
switching src_haskell{case}s on the result of src_haskell{foo}.
Meanwhile, src_haskell{barCPS} is free from such an inefficiency.
Applying this transformation recursively to a whole (sub-)program
allows one to transform the (sub-)program into a series of tail calls
whilst replacing all constructors and eliminators in the (sub-)program
with tail calls to newly introduced continuation arguments and
src_haskell{case} bodies respectively.
The logical mechanic behind this transformation is a technique we call
/generalized Kolmogorov's translation/ (since it is a trivial
extension of Kolmogorov's
translation~\cite{Kolmogorov:1925:OPT:reprint}) of types of functions'
results. That is, double negation followed by rewriting by well-known
isomorphisms until formula contains only arrows, bottoms and variables
followed by generalizing bottoms by a bound variable.
For instance, the result of a function of type
$$i \to j \to b$$
\noindent is $b$, which can be doubly negated as
# NOTE: prettier
@@tex:\newpage@@
$$\lnot \lnot b$$
$$(b \to \bot) \to \bot$$
\noindent and generalized to either of
$$\forall c . (b \to c) \to c$$
$$\lambda c . (b \to c) \to c$$
\noindent which allows us to generalize the whole function to either
of
$$former = \forall c . i \to j \to (b \to c) \to c$$
$$latter = \lambda c . i \to j \to (b \to c) \to c$$
\noindent depending on the desired properties:
- the former term requires a rank-2 type system but it does not add any
new type lambdas or free type variables, thus keeping the
transformation closed,
- the latter term does not need rank-2 types, but it requires tracking
of these new type variables,
- the latter term also retains full control over $c$ variable, (for
instance, it can produce the former term in rank-2 type system on
demand with $\forall c . latter~c$).
Similarly, src_haskell{Either a b} may be seen as logical $a \lor b$
which can be rewritten as
$$\lnot \lnot (a \lor b)$$
$$\lnot (\lnot a \land \lnot b)$$
$$(a \to \bot \land b \to \bot) \to \bot$$
$$(a \to \bot) \to (b \to \bot) \to \bot$$
\noindent and a pair of src_haskell{(a, b)} is logical $a \land b$
and can be rewritten as
$$\lnot \lnot (a \land b)$$
$$\lnot (a \land b) \to \bot$$
$$(a \land b \to \bot) \to \bot$$
$$(a \to b \to \bot) \to \bot$$
Hence, $i \to j \to (a \lor b)$ can be rewritten into either of
$$\forall c . i \to j \to (a \to c) \to (b \to c) \to c$$
$$\lambda c . i \to j \to (a \to c) \to (b \to c) \to c$$
\noindent and $i \to j \to (a \land b)$ into either of
$$\forall c . i \to j \to (a \to b \to c) \to c$$
$$\lambda c . i \to j \to (a \to b \to c) \to c$$
*** Scott-encoding
@@tex:\label{sec:scott-encoding}@@
A technique of applying generalized Kolmogorov's translation to
data types and their constructors and eliminators instead of normal
functions in a (sub-)program is called Scott-encoding (apparently,
Dana Scott did not publish, to our best knowledge the first mention in print
is \cite[p.~219]{Curry:1972:CL2} and first generic description of the
technique for arbitrary data types
is \cite{Steensgaard-Madsen:1989:TRO}).
As before, src_haskell{Either} can be replaced with either of
$$\forall c . (a \to c) \to (b \to c) \to c$$
$$\lambda c . (a \to c) \to (b \to c) \to c$$
\noindent which can be encoded in Haskell as either of
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype EitherS a b = EitherS
{ runEitherS
:: forall c
. (a -> c) -> (b -> c) -> c }
left :: a -> EitherS a b
left a = EitherS (\ac bc -> ac a)
right :: b -> EitherS a b
right b = EitherS (\ac bc -> bc b)
newtype EitherS' c a b = EitherS'
{ runEitherS'
:: (a -> c) -> (b -> c) -> c }
left' :: a -> EitherS' c a b
left' a = EitherS' (\ac bc -> ac a)
right' :: b -> EitherS' c a b
right' b = EitherS' (\ac bc -> bc b)
#+END_SRC
\noindent with src_haskell{runEitherS} (src_haskell{runEitherS'})
taking the role of an eliminator (src_haskell{case} operator) and
src_haskell{left} and src_haskell{right} (src_haskell{left'} and
src_haskell{right'}) taking the roles of src_haskell{Left} and
src_haskell{Right} constructors respectively.
Similarly, src_haskell{(a, b)} can then be generalized to either of
$$\forall c . (a \to b \to c) \to c$$
$$\lambda c . (a \to b \to c) \to c$$
\noindent and encoded in Haskell as either of
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype PairS a b = PairS
{ runPairS
:: forall c
. (a -> b -> c) -> c }
pair :: a -> b -> PairS a b
pair a b = PairS (\f -> f a b)
newtype PairS' c a b = PairS'
{ runPairS'
:: (a -> b -> c) -> c }
pair' :: a -> b -> PairS' c a b
pair' a b = PairS' (\f -> f a b)
#+END_SRC
Substituting all src_haskell{Left}s with src_haskell{left},
src_haskell{Right}s with src_haskell{right}, src_haskell{case}s on
src_haskell{Either}s with src_haskell{runEitherS}, pair constructions
with src_haskell{pair}, and src_haskell{case}s on pairs with
src_haskell{runPairS} (and similarly for primed versions) does not
change computational properties of the transformed program in the
sense that Scott-transformation of the original program's normal form
coincides with the normal form of the Scott-transformed program.
Replacing a single data type in a program with its Scott-encoding can
be viewed as a kind of selective CPS-transform on those subterms of
the program that use the data type. The type of transformed functions
changes the same way in both transformations, but Scott-encoding
groups all continuation arguments, hides them behind a type alias and
introduces a bunch of redundant beta reductions in constructors and
eliminators.
The upside of CPS-transforming with Scott-encoding is that it supports
partial applications, requires absolutely no thought to perform and no
substantial changes to the bodies of the functions that are being
transformed. It is also very useful for designing new languages and
emulating data types in languages that do not support them[fn::For
example, most instances of the /visitor/ object-oriented (OOP) design
pattern that are not simply emulating src_haskell{Functor} instances
usually emulate pattern matching with Scott-encoding.] as it allows to
use data types when none are supported by the core language.
The most immediate downside of this transformation is very poor
performance on modern conventional CPUs. For instance, pattern
matching on src_haskell{Either} produces a simple short conditional
src_assembly{jmp} while for src_haskell{runEitherS} the compiler, in
general, cannot be sure about value of the arguments (it can be
anything of the required type, not only src_haskell{left} or
src_haskell{right}) and has to produce an indirect src_assembly{jmp}
(or src_assemly{call} if it is not a tail call) and both
src_haskell{left} and src_haskell{right} require another indirect
src_assembly{jmp}. This wastes address cache of CPU's branch predictor
and confuses it[fn::Note that this does not happen for the full
CPS-transform of the previous subsection since that translation does
no src_assembly{call}s.] when instruction pointer jumps out of the
stack frame.
For some classes of programs, however, it can increase performance
significantly. For instance, in a "/src_haskell{case}-tower/" like
#+BEGIN_SRC haskell-spec
doSomethingOn s = case internally s of
Right a -> returnResult a
Left b -> handeError b
internally s =
case evenMoreInternally s of
Right (a,s) -> doSomethingElse a s
Left b -> Left b
doSomethingElse a s =
case evenMoreInternally s of
Right (a,s) -> Right a
Left b -> Left b
#+END_SRC
\noindent (which is commonly produced by parser combinators)
performing this selective CPS-transform followed by inlining and
partial evaluation of the affected functions will replace all
construction sites of src_haskell{Left}s with direct calls to
src_haskell{handeError}, and src_haskell{Right}s in
src_haskell{doSomethingElse} (and, possibly, the ones residing in
src_haskell{evenMoreInternally}) with src_haskell{returnResult}.
In other words, rewriting this type of code using Scott-encoded
data types is a way to apply deforestation~\cite{Wadler:1990:DTP} to
it, but semi-manually as opposed to automatically, and with high
degree of control. This fact gets used a lot in Hackage libraries,
where, for example, most parser combinators
(\cref{sec:parser-combinators}) use Scott-encoded forms internally.
*** src_haskell{Cont}
@@tex:\label{sec:cont}@@
One of the roundabout ways to express pure values in Haskell is to
wrap them with the src_haskell{Identity} src_haskell{Functor}
(\cref{sec:identity}) for which src_haskell{Identity a}, logically, is
just a pure type variable $a$. Applying generalized Kolmogorov's
translation to this variable gives either of
$$\forall c . (a \to c) \to c$$
$$\lambda c . (a \to c) \to c$$
In Haskell the latter type is called src_haskell{Cont}. It is defined
in src_haskell{Control.Monad.Cont} of =mtl=~\cite{Hackage:mtl221} as
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype Cont r a = Cont
{ runCont :: (a -> r) -> r }
#+END_SRC
\noindent with the following src_haskell{Monad} instance
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Pointed (Cont r) where
pure a = Cont $ \c -> c a
instance Monad (Cont r) where
m >>= f = Cont $ \c -> runCont m
$ \a -> runCont (f a) c
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor (Cont r) where
fmap = liftM
instance Applicative (Cont r) where
(<*>) = ap
#+END_SRC
src_haskell{Cont} has a transformer version defined in
src_haskell{Control.Monad.Trans.Cont} module of
=transformers=~\cite{Hackage:transformers0520} package as follows
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
newtype ContT r m a = ContT { runContT :: (a -> m r) -> m r }
instance MonadTrans (ContT' r) where
lift m = ContT (m >>=)
#+END_SRC
Interestingly, however, unlike src_haskell{Identity} and
src_haskell{IdentityT} which have different src_haskell{Monad}
instances (see \cref{sec:identity-monadtrans}), src_haskell{Cont} and
src_haskell{ContT} have identical ones (equivalent to the one given
above). Of particular note is the fact that the definition of
src_haskell{(>>=)} for src_haskell{ContT} does not refer to the
src_haskell{Monad} operators of its argument src_haskell{m}. This
means that in cases when we do not need the src_haskell{MonadTrans}
instance (for which we have to have a src_haskell{newtype} wrapper) we
can redefine src_haskell{ContT} as simply
#+BEGIN_SRC haskell :tangle tng-main.hs
type ContT r m a = Cont (m r) a
#+END_SRC
The latter fact means that src_haskell{ContT}, unlike other
src_haskell{MonadTrans}formers we saw before, is not a
"src_haskell{Monad} transformer" as it is not a functor on category of
monads (it is always a src_haskell{Monad} irrespective of the argument
src_haskell{m}). This property can be explained by the fact that, as
we noted at the top of this section, src_haskell{Cont}
src_haskell{Monad} is a kind of /"implicit-CPS"/ form of computations.
Since all it does is chain return addresses it does not care about
types of computations those addresses point to.
*** Delimited src_haskell{callCC}
@@tex:\label{sec:callcc}@@
Peirce's law states that
$$((a \to b) \to a) \to a$$
\noindent by applying generalized Kolmogorov's translation we get
$$\lnot \lnot (((a \to b) \to a) \to a)$$
$$\lnot (\lnot a \to \lnot ((a \to b) \to a))$$
$$\lnot \lnot ((a \to b) \to a) \to \lnot \lnot a$$
$$(\lnot \lnot (a \to b) \to \lnot \lnot a) \to \lnot \lnot a$$
$$((\lnot \lnot a \to \lnot \lnot b) \to \lnot \lnot a) \to \lnot \lnot a$$
\noindent which can be encoded in Haskell as (note that this time we
use $\forall$ variant of the translation)
#+BEGIN_SRC haskell :tangle tng-main.hs
peirceCC :: ((Cont r a -> Cont r b) -> Cont r a)
-> Cont r a
peirceCC f = Cont $ \c ->
runCont (f (\ac -> Cont $ \_ -> runCont ac c)) c
#+END_SRC
This operator takes a function src_haskell{f}, applies some magical
subterm to it and then gives it its own return address. That is, for a
function src_haskell{f} that ignores its argument
src_haskell{peirceCC} is completely transparent. The magical argument
src_haskell{peirceCC} applies to src_haskell{f} is itself a function
that takes a computation producing value of the same type
src_haskell{f} returns as a result. The subterm then computes the
value of the argument but ignores its own return address and continues
to the return address given to src_haskell{peirceCC} instead. In other
words, src_haskell{peirceCC} applies src_haskell{f} with an /escape
continuation/ which works exactly like a src_c{return} statement of
conventional imperative languages (as opposed to src_haskell{Monad}'s
src_haskell{pure} which should not be called "src_haskell{return}",
see \cref{sec:monad}).
Note that src_haskell{ac} argument to the magical subterm is pretty
boring: it is a computation that gets computed immediately. Hence,
unless we require every subterm of our program to be written in
/implicit-CPS/ form we can simplify src_haskell{peirceCC} a bit as
follows
#+BEGIN_SRC haskell :tangle tng-main.hs
callCC :: ((a -> Cont r b) -> Cont r a) -> Cont r a
callCC f = Cont $ \c ->
runCont (f (\a -> Cont $ \_ -> c a)) c
#+END_SRC
This operator bears a name of "delimited src_scheme{call/cc}
(src_scheme{callCC})"~\cite{Asai:2011:IPS} and the escape continuation
it supplies to src_haskell{f} not only works but also looks exactly
like an imperative src_c{return} (in that it takes a pure value
instead of a computation producing it).
*** Scheme's src_scheme{call/cc} and ML's src_ocaml{callcc}
Note that delimited src_haskell{callCC} is semantically different from
similarly named operators of SML~\cite{SML:Cont} and
Scheme~\cite{Sperber:2010:RnRS}. SML defines its operator as
#+BEGIN_SRC ocaml-spec
type 'a cont
val callcc : ('a cont -> 'a) -> 'a
#+END_SRC
\noindent where src_ocaml{'a cont} type is the type of the /current
global continuation/ which is the computation till the end of the
whole program, this type is a kind of technical alias for what,
logically, should be $a \to b$, i.e. src_ocaml{callcc}'s type,
logically, is non-Kolmogorov-translated Peirce's law.
The difference is that by applying Kolmogorov's translation to
Peirce's law src_haskell{callCC} gains intuitionistic witnesses (and,
hence, purely functional implementations) and becomes /delimited/ by
the current src_haskell{Cont} context instead of the whole program.
Meanwhile, implementations of non-delimited src_ocaml{callcc} and
src_scheme{call/cc} require special support from the
compiler/interpreter and Kiselyov~\cite{Kiselyov:2012:AAC} eloquently
advocates that they simply should not exist as they are /less/ useful
than their delimited versions and their implementations introduce
nontrivial trade-offs to the languages in question.
# NOTE: You may also want to lookup =shift=, =reset=, polar logic,
# Shan, Zeilberger. There are more things worth mentioning here, but
# this is not a book.
** src_haskell{Monad}ic Parser Combinators
@@tex:\label{sec:parser-combinators}@@
src_haskell{Monad}ic parser combinators are not by themselves an error
handling mechanism, but they have to handle failed parsing attempts
and such computations can be seen as a kind of error handling.
Parser combinators can possess a wide variety of semantics and
implementations, to mention just a few possible dimensions of the
space:
- they can either automatically backtrack on errors or keep the state
as is,
- they can distinguish not only successful and failed parsing attempts
but also attempts that consumed none of the input and those that
consumed at least one element of the input~\cite{Leijen:2001:PDS},
- they can support an impure state (e.g., make it a src_haskell{Monad}),
- track position in the input stream,
- allow programmer-provided types in errors,
- provide src_haskell{MonadTrans}former versions,
- encode their internals with Scott-encoding
(\cref{sec:scott-encoding}) for efficiency.
Discussing most of those features and their combinations is beyond the
scope of this article. In the following subsections we shall only
mention "backtrack vs. not" problem, in \cref{sec:instances:eio} we
shall also apply Scott-encoding to an almost identical structure.
Detailed implementations of other features can be studied by following
respective references.
The most popular parser combinator libraries for Haskell are
Parsec~\cite{Hackage:parsec3111},
Attoparsec~\cite{Hackage:attoparsec01310}, and
Megaparsec~\cite{Hackage:megaparsec630}.
*** Simple stateful parser combinator
@@tex:\label{sec:parser-combinators:without-access}@@
The simplest src_haskell{Monad}ic parser combinator is just a
composition of src_haskell{StateT}
(\cref{sec:reader-state-monadtrans}) and src_haskell{ExceptT}
(\cref{sec:either-monadtrans}) src_haskell{MonadTrans}formers with
inner src_haskell{Identity} (\cref{sec:identity})
#+BEGIN_SRC haskell-spec
type SParser s e = StateT s (ExceptT e Identity)
#+END_SRC
\noindent which can be $\beta$-reduced into
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype SParser s e a = SParser
{ runSParser :: s -> Either e (a, s) }
#+END_SRC
\noindent with the following src_haskell{Monad} instance
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Pointed (SParser s e) where
pure a = SParser $ \s -> Right (a, s)
instance Monad (SParser s e) where
p >>= f = SParser $ \s ->
case runSParser p s of
Left x -> Left x
Right (a, s') -> runSParser (f a) s'
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor (SParser s e) where
fmap = liftM
instance Applicative (SParser s e) where
(<*>) = ap
#+END_SRC
*** \dots with full access to the state
@@tex:\label{sec:parser-combinators:with-access}@@
While the definition above is, in fact, exactly the definition used in
=ponder=~\cite{Hackage:ponder001} parser combinator library, it
provides no way to access the state of the parser on error, which
makes it very inconvenient in practice. However, a simple modification
of the type that moves src_haskell{Either} into the tuple
#+BEGIN_SRC haskell-spec
newtype Parser s e a = Parser
{ runParser :: s -> (Either e a, s) }
#+END_SRC
\noindent which, of course, in isomorphic to[fn::The corresponding
src_haskell{MonadTrans}former stack is better left unspoken.]
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype Parser s e a = Parser
{ runParser :: s -> Either (e, s) (a, s) }
#+END_SRC
\noindent solves this problem of access to state while keeping the
definition of src_haskell{Monad} identical to the above.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- yep, copy-paste
instance Pointed (Parser s e) where
pure a = Parser $ \s -> Right (a, s)
instance Monad (Parser s e) where
p >>= f = Parser $ \s ->
case runParser p s of
Left x -> Left x
Right (a, s') -> runParser (f a) s'
instance Functor (Parser s e) where
fmap = liftM
instance Applicative (Parser s e) where
(<*>) = ap
#+END_SRC
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_theorem
src_haskell{Parser} satisfies src_haskell{Monad} laws.
#+END_theorem
#+BEGIN_proof
By case analysis. Also see the next proof.
#+END_proof
The binary /choice/ operator can be implemented by one of the two
possible instances of src_haskell{Alternative}. The first one
rolls-back the state on error
#+BEGIN_SRC haskell :tangle tng-main.hs
instance Monoid e => Alternative (Parser s e) where
empty = Parser $ \s -> Left (mempty, s)
f <|> g = Parser $ \s -> case runParser f s of
Right x -> Right x
Left (e, _) -> case runParser g s of
Right x -> Right x
Left (f, _) -> Left (e `mappend` f, s)
#+END_SRC
\noindent while the second does not
#+BEGIN_SRC haskell-spec
instance Monoid e => Alternative (Parser s e) where
empty = Parser $ \s -> Left (mempty, s)
f <|> g = Parser $ \s -> case runParser f s of
Right x -> Right x
Left (e, s') -> case runParser g s' of
Right x -> Right x
Left (f, s'') -> Left (e `mappend` f, s'')
#+END_SRC
#+BEGIN_theorem
@@tex:\label{thm:with-heuristic}@@
Both versions satisfy the laws of
src_haskell{Alternative}.[fn::Note, however, that
src_haskell{SParser} from
\cref{sec:parser-combinators:without-access} can only do
backtracking because, unlike src_haskell{Parser}, it is asymmetric
in its use of src_haskell{Either}.]
#+END_theorem
#+BEGIN_proof
By case analysis.
Note that to convince yourself that src_haskell{(<|>)} is associative
it is enough to observe that in src_haskell{a <|> b <|> c} for the
above definitions
- src_haskell{Right} is a zero,
- values of src_haskell{e} always propagate to the right,
- while src_haskell{s} is stays constant in the roll-back version, or
always propagates in the no-roll-back version, but never both.
Which means that parentheses can't influence anything in either case.
The same idea can be used in similar proofs involving similar
operators of src_haskell{State} and src_haskell{Parser}.
#+END_proof
From the popular Haskell parser combinator libraries mentioned above
Attoparsec rolls-back while Parsec and Megaparsec do not, instead they
implement backtracking with a separate combinator for which we could
give the following type signature
#+BEGIN_SRC haskell-spec
try :: Parser s e a -> Parser s e a
#+END_SRC
*** Examples
@@tex:\label{sec:parser-combinators:examples}@@
The already given definitions allow us enough headroom to define some
primitive parsers and a couple of examples. For instance, assuming
src_haskell{Alternative} rolls-back we can write
#+BEGIN_SRC haskell :tangle tng-main.hs
type Failures = [String]
eof :: Parser String Failures ()
eof = Parser $ \s -> case s of
[] -> Right ((), s)
_ -> Left (["expected eof"], s)
char :: Char -> Parser String Failures ()
char x = Parser $ \s -> case s of
[] -> Left (["unexpected eof"], s)
(c:cs) -> if (c == x)
then Right ((), cs)
else Left (["expected `" ++ [x] ++ "' got `" ++ [c] ++ "'"], s)
string :: String -> Parser String Failures ()
string [] = pure ()
string (c:cs) = char c >> string cs
parseTest = runParser (string "foo") "foo bar"
== Right((), " bar")
&& runParser (string "abb" <|> string "abc") "aba"
== Left (["expected `b' got `a'"
,"expected `c' got `a'"], "aba")
#+END_SRC
To use the other implementation of src_haskell{Alternative} we would
need to wrap all calls to src_haskell{string} on the left hand sides
of src_haskell{(<|>)} with src_haskell{try}s.
Semantics-wise our src_haskell{Parser} combines features of Attoparsec
(backtracking) and Megaparsec (custom error types). Of course, it fits
on a single page only because it has a minuscule number of features in
comparison to either of the two. To make it practical we would need,
at the very least, to implement tracking of the position in the input
stream and a bunch of primitive parsers, which we leave as an exercise
to the interested reader.
Interestingly, this exact implementation of handling of errors by
accumulation via src_haskell{Alternative} over a src_haskell{Monoid}
seems to be novel (although, pretty trivial). Megaparsec, however,
does something very similar by accumulating errors in
src_haskell{Set}s instead of src_haskell{Monoid}s.
src_haskell{MonadTrans}former versions of these structures can be
trivially obtained by adding src_haskell{Monad}ic index src_haskell{m}
after the arrow in definition of src_haskell{Parser} (i.e. by exposing
the internal src_haskell{Monad} of the original
src_haskell{MonadTrans} stack) and correspondingly tweaking base-level
definitions and all type signatures.
** Other variants of src_haskell{MonadCatch}
@@tex:\label{sec:other-monadic-generalizations}@@
Finally, worth mentioning are two lesser-known variants of structures
similar to structures of \cref{sec:monadic-generalizations}. The first
one is defined in src_haskell{Control.Monad.Exception.Catch} module of
=control-monad-exception=~\cite{Hackage:control-monad-exception0112}
package as
#+BEGIN_SRC haskell-spec
class (Monad m, Monad n) => MonadCatch e m n | e m -> n, e n -> m where
catch :: m a -> (e -> n a) -> n a
#+END_SRC
\noindent and the second one in src_haskell{Control.Monad.Catch.Class}
module of =catch-fd=~\cite{Hackage:catch-fd0202} package
#+BEGIN_SRC haskell-spec
class Monad m => MonadThrow e m | m -> e where
throw :: e -> m a
class (MonadThrow e m, Monad n) => MonadCatch e m n | n e -> m where
catch :: m a -> (e -> n a) -> n a
#+END_SRC
Note that =control-monad-exception= does not define a type class with
a src_haskell{throw} operator, that library provides a universal
computation type src_haskell{EM} (similar to src_haskell{EIO} of
\cref{sec:instances:eio}) with such an operator instead. Also note
that the common point of those two definitions is that both
src_haskell{catch} operators change the type of computations from
src_haskell{m} to src_haskell{n}.
* The nature of an error
@@tex:\label{sec:init}@@
#+BEGIN_SRC haskell :tangle tng-derivation.hs :exports none
{-# LANGUAGE NoImplicitPrelude, RankNTypes #-}
import Prelude ((.), ($), undefined)
#+END_SRC
Lets forget for a minute about every concrete algebraic error-handling
structure mentioned before and try to invent our own algebra of
computations by reasoning like a purely pragmatic programmer who
likes to make everything typed as precisely as possible.
We start, of course, by pragmatically naming our type of computations
to be src_haskell{C}. Then, we reason, it should be indexed by both
the type of the result, which we shall pragmatically call
src_haskell{a}, and the type of exceptions src_haskell{e}. We are not
sure about the body of that definition, so we just leave it undefined
#+BEGIN_SRC haskell :tangle tng-derivation.hs
data C e a
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-derivation.hs :exports none
--
= UndefinedC
#+END_SRC
Now, we know that src_haskell{Monad}s usually work pretty well for the
computation part (since we can as well just lift everything into
src_haskell{IO} which is a src_haskell{Monad}), so we write
#+BEGIN_SRC haskell :tangle tng-derivation.hs
return :: a -> C e a
(>>=) :: C e a -> (a -> C e b) -> C e b
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-derivation.hs :exports none
return = undefined
(>>=) = undefined
#+END_SRC
\noindent and expect these operators to satisfy src_haskell{Monad}
laws (\cref{sec:monad}).
Meanwhile, pragmatically, an "exceptional" execution path requires two
conventional operators:
- a method of raising an exception; the type of this operator seems to
be pretty straightforward
#+BEGIN_SRC haskell :tangle tng-derivation.hs
throw :: e -> C e a
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-derivation.hs :exports none
throw = undefined
#+END_SRC
as it simply injects the error into src_haskell{C},
- and a method to catch exceptions; the overly-general type for this
operator is, again, pretty straightforward
#+BEGIN_SRC haskell-spec
catch :: C e a -> (e -> C f b) -> C g c
#+END_SRC
The only obvious requirement here is that the type the "handler"
function (the second argument of src_haskell{catch}) can handle
should coincide with the type of errors the "computation" (the first
argument) can src_haskell{throw}.
Finally, we pragmatically expect the above to obey the conventional
operational semantics of error handling operators, giving us the
following definition.
#+BEGIN_definition
@@tex:\label{dfn:structure}@@
**Pragmatic error handling structure.**
Structure src_haskell{m :: * => * => *} with src_haskell{return},
src_haskell{(>>=)}, src_haskell{throw}, and src_haskell{catch}
operators satisfying
1. @@tex:\label{dfn:structure:monad}@@
src_haskell{return} and src_haskell{(>>=)} obey src_haskell{Monad}
laws (\cref{sec:monad}),
2. @@tex:\label{dfn:structure:throw-bind}@@
src_haskell{throw e >>= f == throw e}
("src_haskell{throw}ing of an error stops the computation"),
3. @@tex:\label{dfn:structure:throw-catch}@@
src_haskell{throw e `catch` f == f e}
("src_haskell{throw}ing of an error invokes the most recent error
handler"),[fn::Similarly to GHC's imprecise exceptions of
\cref{sec:imprecise} dynamic dispatch can be implemented on top of
such a structure. We shall do this in
\cref{sec:instances:constant:monadcatch}.]
4. @@tex:\label{dfn:structure:return-catch}@@
src_haskell{return a `catch` f == return a} ("src_haskell{return}
is not an error").
#+END_definition
* The type of error handling operator
@@tex:\label{sec:type-of-catch}@@
The first question to the structure of src_haskell{C} is, of course,
what is the precise type of src_haskell{catch} operator.
#+BEGIN_SRC haskell-spec
catch :: C e a -> (e -> C f b) -> C g c
#+END_SRC
\noindent In other words, we would like to know which of the variables
src_haskell{f}, src_haskell{g}, src_haskell{b}, and src_haskell{c} in
this signature should have their own universal quantifier and which
should be substituted with others. The answer comes by considering
several cases.
- Firstly, let us consider the following expression.
#+BEGIN_SRC haskell-spec
return a `catch` f
#+END_SRC
The expected semantics of src_haskell{catch} requires (by
\cref{dfn:structure:return-catch} of \cref{dfn:structure})
#+BEGIN_SRC haskell-spec
return a `catch` f == return a
#+END_SRC
Note that the most general type for src_haskell{return a} expression
is src_haskell{forall e . C e a} for src_haskell{a : a}[fn::The
reader might have noticed already that we abuse notation somewhat by
assuming type variables and term variables use distinct namespaces.
This expression happens to be the first and the only one that uses
both at the same time, hence it looks like an exiting "type-in-type"
kind of thing, but it is not, it is ordinarily boring.]. Moreover,
we can assign the same type to any expression that does not
src_haskell{throw} since
- both src_haskell{a} and src_haskell{e} in the type signify the
potential to src_haskell{return} and src_haskell{throw} values of
the corresponding types,
- and an expression that does not src_haskell{throw} any errors can
be said to not-src_haskell{throw} an error of any particular type,
similarly to how bottom elimination rule works. Or, equivalently,
any such computation can be said to src_haskell{throw} values of
an empty type and an empty type can always be replaced with any
other type by bottom elimination.[fn::Implicitly or with
src_haskell{f `catch` bot-elim} which is extentionally equal
to src_haskell{f}.]
- Now let us consider the following expression, assuming
src_haskell{e} and src_haskell{f} are of different types (i.e. both
the computation and the handler throw different exceptions).
#+BEGIN_SRC haskell-spec
throw e `catch` (\_ -> throw f)
#+END_SRC
The expected semantics of src_haskell{catch} requires (by
\cref{dfn:structure:throw-catch} of \cref{dfn:structure})
#+BEGIN_SRC haskell-spec
throw e `catch` (\_ -> throw f) == throw f
#+END_SRC
These two cases show that src_haskell{g} should be substituted with
src_haskell{f} and src_haskell{e} should be kept separate from
src_haskell{f} because
- if computation src_haskell{throw}s then the type src_haskell{f} in
the handler "wins",
- but if it does not src_haskell{throw} then src_haskell{e} is an empty
type and it can be substituted for any other type, including
src_haskell{f} (similarly to the type of src_haskell{return}
above)[fn::The only nontrivial observation in this section.]
- these two cases are mutually exclusive.
That is, the type for src_haskell{catch} is at most as general as
#+BEGIN_SRC haskell-spec
catch :: forall e f . C e a -> (e -> C f b) -> C f c
#+END_SRC
- Continuing, \cref{dfn:structure:return-catch} of
\cref{dfn:structure} shows that src_haskell{c} has to coincide with
src_haskell{a}.
- Similarly, \cref{dfn:structure:throw-catch} requires
#+BEGIN_SRC haskell-spec
throw e `catch` (\_ -> return a) == return a
#+END_SRC
which shows that src_haskell{c} has to coincide with src_haskell{b}.
All these observations combine into the
following.[fn::@@tex:\label{fn:its-dual}@@Spoilers! The reader is
only supposed to notice the following after reading
\cref{sec:logical}.\\
\\
Note that we could have written an equivalent up to names of operators
sections~\ref{sec:init} and~\ref{sec:type-of-catch} that explained why
the type of src_haskell{(>>=)} is the correct type for sequencing
computations in src_haskell{C} given that error handling should be
done src_haskell{Monad}ically. In particular, the fact that the dual
of \cref{dfn:structure} lists valid operational equations is a rather
curious observation by itself. Which is another reason why we disagree
with the conventional wisdom in footnote~\ref{fn:terms}.]
#+BEGIN_theorem
@@tex:\label{thm:catch-type}@@
For any type src_haskell{C :: * => * => *} obeying
\cref{dfn:structure} the most general type for the src_haskell{catch}
operator is
#+BEGIN_SRC haskell :tangle tng-derivation.hs
catch :: forall a e f . C e a -> (e -> C f a) -> C f a
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-derivation.hs :exports none
catch = undefined
#+END_SRC
#+END_theorem
#+BEGIN_proof
By the above reasoning. That is, by simple unification of types of
src_haskell{return}, src_haskell{throw}, src_haskell{(>>=)} operators
of \cref{dfn:structure} and the following equations that are
consequences of equations of \cref{dfn:structure}
#+BEGIN_SRC haskell-spec
return a `catch` f == return a
throw e `catch` (\_ -> return a) == return a
throw e `catch` (\_ -> throw f) == throw f
#+END_SRC
#+END_proof
* Conjoinedly src_haskell{Monad}ic algebra
@@tex:\label{sec:conjoinedly-monadic}@@
After \cref{thm:catch-type} it becomes hard to ignore the fact that
src_haskell{throw} has the type of src_haskell{return} and
src_haskell{catch} has the type of src_haskell{(>>=)} in the "wrong"
index for src_haskell{C}. Moreover, \cref{dfn:structure:throw-catch}
of \cref{dfn:structure} looks exactly like a left identity law for
src_haskell{Monad} (\cref{sec:monad}). While it is not as immediately
clear that src_haskell{catch} should be associative, it seems only
natural to ask whenever the following conjoinedly src_haskell{Monad}ic
restriction of \cref{dfn:structure} has any instances.
#+BEGIN_definition
@@tex:\label{dfn:proper}@@
**Conjoinedly monadic error algebra**.
A type src_haskell{m :: * => * => *} for which
- @@tex:\label{dfn:proper:bind-monad}@@
src_haskell{m} is a src_haskell{Monad} in its second index (that is,
src_haskell{m e} is a src_haskell{Monad} for all src_haskell{e}),
- @@tex:\label{dfn:proper:catch-monad}@@
src_haskell{m} is a src_haskell{Monad} in its first index (that is,
src_haskell{\e . m e a} is a src_haskell{Monad} for all
src_haskell{a}),
and assuming
- the names of src_haskell{Monad} operators in the second index of
src_haskell{m} are src_haskell{return} and src_haskell{(>>=)},
- the names of src_haskell{Monad} operators in the first index are
src_haskell{throw} and src_haskell{catch},
the following equations hold
1. @@tex:\label{dfn:proper:return-catch}@@
src_haskell{return x `catch` f == return x},
2. @@tex:\label{dfn:proper:throw-bind}@@
src_haskell{throw e >>= f == throw e}.
#+END_definition
If we replace src_haskell{Monad} in \cref{dfn:proper} with
src_haskell{MonadFish} (\cref{sec:monad-fish}), as usual, the latter
two equations become a bit clearer.
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_definition
@@tex:\label{dfn:fishy}@@
**Fishy conjoinedly monadic error algebra**. A type src_haskell{m :: * => * => *}
for which
- @@tex:\label{dfn:fishy:bind-monad}@@
src_haskell{m} is a src_haskell{MonadFish} in its second index,
- @@tex:\label{dfn:fishy:catch-monad}@@
src_haskell{m} is a src_haskell{MonadFish} in its first index,
and assuming
- the names of src_haskell{MonadFish} operators in the second index
are src_haskell{return} and src_haskell{(>=>)},
- the names of src_haskell{MonadFish} operators in the first index are
src_haskell{throw} and src_haskell{handle},
the following equations hold
1. @@tex:\label{dfn:fishy:return-catch}@@
src_haskell{return `handle` f == return},
2. @@tex:\label{dfn:fishy:throw-bind}@@
src_haskell{throw >=> f == throw}.
#+END_definition
On other words, definitions~\ref{dfn:proper} and~\ref{dfn:fishy}
define a structure that is a src_haskell{Monad}
(src_haskell{MonadFish}) twice and for which src_haskell{return} is a
left zero for src_haskell{catch} (src_haskell{handle}) and
src_haskell{throw} is a left zero for src_haskell{(>>=)}
(src_haskell{(>=>)}).
* Instances: src_haskell{Either}
@@tex:\label{sec:instances:either}@@
Pragmatic programmer finally loses last bits of concentration
realizing that src_haskell{Either} type seems to match requirements of
\cref{dfn:proper} and goes into sources to check whenever Haskell's
standard library already has such a src_haskell{catch}. Unfortunately,
src_haskell{Data.Either} module does not define such an operator.
However, src_haskell{catchE} and src_haskell{throwE} of
src_haskell{ExceptT} (\cref{sec:either-monadtrans}) match. Of course,
if we substitute src_haskell{Identity} for src_haskell{m},
src_haskell{ExceptT} turns into src_haskell{Either} and those
operators can be simplified to
#+BEGIN_SRC haskell :tangle tng-main.hs
throwE' :: e -> Either e a
throwE' = Left
catchE' :: Either e a
-> (e -> Either f a)
-> Either f a
catchE' (Left e) h = h e
catchE' (Right a) _ = Right a
#+END_SRC
#+BEGIN_lemma
@@tex:\label{thm:ExceptT-monad}@@
For a given src_haskell{Monad} src_haskell{m} and a fixed argument
src_haskell{a}, src_haskell{ExceptT} with src_haskell{throwE} as
src_haskell{return} and src_haskell{catchE} as src_haskell{(>>=)} is
a src_haskell{Monad} in argument src_haskell{e}.
#+END_lemma
#+BEGIN_proof
Any of the following
- **By brute force:** by case analysis, using the fact that src_haskell{m}
satisfies src_haskell{Monad} laws.
- **Another way:** trivial consequence of \cref{sec:logical}.
#+END_proof
#+BEGIN_lemma
@@tex:\label{thm:ExceptT-zeroes}@@
For src_haskell{ExceptT} with the above operators the following
equations hold
1. src_haskell{return x `catchE` f == return x},
2. src_haskell{throwE e >>= f == throwE e}.
#+END_lemma
#+BEGIN_proof
By trivial case analysis.
#+END_proof
#+BEGIN_theorem
@@tex:\label{thm:ExceptT-proper}@@
src_haskell{ExceptT} and, by consequence, src_haskell{Either} satisfy \cref{dfn:proper}.
#+END_theorem
#+BEGIN_proof
Consequence of \cref{thm:ExceptT-monad} and \cref{thm:ExceptT-zeroes}.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Let us also typecheck it
instance ConjoinedMonads Either where
creturn = return
cbind = (>>=)
cthrow = throwE'
ccatch = catchE'
#+END_SRC
#+END_proof
* Logical perspective
@@tex:\label{sec:logical}@@
Note, that from a logical perspective most of the above is simply
trivial.
src_haskell{Either a b} is just
$a \lor b$
and so if
$\lambda b . a \lor b$
is a src_haskell{Monad} then
$\lambda a . a \lor b$
must be a src_haskell{Monad} too since $\lor$ operator is symmetric.
Sections~\ref{sec:init}-\ref{sec:conjoinedly-monadic} simply generalize
this fact with interactions between src_haskell{Left},
src_haskell{Right} and two src_haskell{(>>=)} operators into
\cref{dfn:proper}.\cref{fn:its-dual}
The main point of this article is that **there are other instances**
of this generalization and, more importantly, that **this
generalization is itself interesting** --- the facts that we shall
demonstrate in the sections that follow.
* Encodings
@@tex:\label{sec:encodings}@@
Despite the noted triviality, these facts do not seem to be
appreciated by the wider Haskell community. In particular:
- src_haskell{ExceptT} does not get much use in Hackage packages in
general,
- the equivalent of src_haskell{catchE} for src_haskell{ErrorT} has an
overly-restricted type
#+BEGIN_SRC haskell :tangle tng-syntax-originals.hs
catchError :: (Monad m)
=> ErrorT e m a
-> (e -> ErrorT e m a)
-> ErrorT e m a
m `catchError` h = ErrorT $ do
a <- runErrorT m
case a of
Left l -> runErrorT (h l)
Right r -> return (Right r)
#+END_SRC
- no src_haskell{Monad}ic parsing combinator library from Hackage
(most obvious beneficiaries of the observation) defines the
would-be-src_haskell{Monad} instance of src_haskell{throwE} and
src_haskell{catchE}.
To our best knowledge, the only Hackage package that is explicitly
aware of the fact that src_haskell{Either} is a src_haskell{Monad}
twice is =errors=~\cite{Hackage:errors230}[fn::
In~\cite{Gonzalez:2012:SEH} Gabriel Gonzalez, the author of the
=errors= package, also explicitly mentions the fact that the
src_haskell{Monad}ic operators for the other index of
src_haskell{Either} seem to match the semantics for the corresponding
src_haskell{throw} and src_haskell{catch} operators. Though he gives
no proofs or claims of general applicability, he mentions that the
fact itself was first pointed out to him by Elliott Hird who named it
the "success src_haskell{Monad}". So, though the Net seems to have no
evidence of that conversation, it is entirely possible some of the
discussed facts were already discovered in their complete forms before
(at least in the idealistic sense, but not, to our best knowledge, in
the "communicated in this form before" sense). (Which is usually the
case for almost anything anyway.) (Which is a yet another reminder
that "intellectual property" is an oxymoron.)] and the only packages
that seem to be aware that src_haskell{throw} and src_haskell{catch}
in general need more general types than those given by
src_haskell{MonadCatch} of \cref{sec:monadic-generalizations} are
those discussed in \cref{sec:other-monadic-generalizations} (but they
miss the fact that their src_haskell{catch} operators want to be
src_haskell{Monad}ic src_haskell{bind}s). To our best knowledge, no
Hackage package utilizes both facts.
As to the question why had not anybody notice and start exploiting
these facts yet we hypothesize that the answer is because Haskell
cannot express these properties conveniently (not to mention less
expressive mainstream languages which cannot express them at all).
The simplest possible encoding of \cref{dfn:proper} in Haskell is just
#+BEGIN_SRC haskell-spec
class ConjoinedMonads m where
return :: a -> m e a
(>>=) :: m e a -> (a -> m e b) -> m e b
throw :: e -> m e a
catch :: m e a -> (e -> m f a) -> m f a
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- For typechecking signatures used in proofs
class ConjoinedMonads m where
creturn :: a -> m e a
cbind :: m e a -> (a -> m e b) -> m e b
cthrow :: e -> m e a
ccatch :: m e a -> (e -> m f a) -> m f a
#+END_SRC
\noindent but it does not play too well with the rest of the Haskell
ecosystem. In the ideal world, \cref{dfn:proper} would get encoded
with the following pseudo-Haskell definition
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_definition
@@tex:\label{dfn:proper-haskell}@@
**Proper pseudo-Haskell definition.**
#+BEGIN_SRC haskell-spec
class (forall a . Monad (\e -> m e a)) -- `Monad` in `e`
, forall e . Monad (m e) -- `Monad` in `a`
=> ConjoinedMonads m where
-- and that's it
#+END_SRC
#+END_definition
\noindent however, Haskell allows neither rank 2 types in type
classes, nor lambdas in types, which brings us to the following
"theorem".
#+BEGIN_quasitheorem
@@tex:\label{thm:not-in-haskell}@@
Haskell cannot properly (equivalently to \cref{dfn:proper-haskell})
define src_haskell{ConjoinedMonads}.
#+END_quasitheorem
#+BEGIN_proof
Proper definition of src_haskell{ConjoinedMonads} requires rank 2
types in type class declaration, which is not possible in modern
Haskell. There is no way to emulate rank 2 definition using only rank 1
constructions.
#+END_proof
# TODO(low): cite something above?
We call it a "theorem" because we do not really know if its proof
really works out for Haskell as Haskell has an awful lot of language
extensions (including future ones) and there might be some nontrivial
combination of those that gives the desired effect. In particular, GHC
version 8.6 released just before this article was finished introduced
=QuantifiedConstraints= extension~\cite{Bottu:2017:QCC} allowing us to
write
#+BEGIN_SRC haskell-spec
data Swap r a e = Swap { unSwap :: r e a }
instance (forall e . Monad (r e)
, forall a . Monad (Swap r a))
=> ConjoinedMonads r where
-- ...
#+END_SRC
\noindent which, arguably, can be considered good enough, though not
very convenient in practice.
The purposes of this article, however, is not to demonstrate that
there is a convenient form of \cref{dfn:proper} in Haskell but to show
what could be achieved if there were such a convenient definition.
Which means that we can and, hence, shall completely ignore the
question of the most elegant Haskell representation for
\cref{dfn:proper} and just use the very first definition of
src_haskell{ConjoinedMonads} from above for simplicity.
As to the naming, it is, indeed, tempting to call this structure
src_haskell{BiMonad}, but that name is already taken by another
structure from category theory. Then, since the structure consists of
two src_haskell{Monads} that are "dual" to each other via interaction
laws it is tempting to call it src_haskell{DualMonad} as a double-pun,
but that "duality" is different from the usual duality of category
theory. Which is why we opted into using the name
"src_haskell{ConjoinedMonads}" (in the sense of "conjoined twins",
conjoined with left-zeroes).
* Instances: constant src_haskell{Functor}s
@@tex:\label{sec:instances:constant}@@
In this section we discuss the relationship between
src_haskell{ConjoinedMonads} (and \cref{dfn:proper}) and
src_haskell{MonadThrow}, src_haskell{MonadCatch}, and
src_haskell{MonadError} from \cref{sec:monadic-generalizations}.
** src_haskell{MonadError}
@@tex:\label{sec:instances:constant:monaderror}@@
src_haskell{MonadError} (\cref{sec:monad-error}) relationship to
src_haskell{ConjoinedMonads} turns out to be pretty simple. Remember that
src_haskell{MonadError} is defined using functional dependencies
#+BEGIN_SRC haskell-spec
class (Monad m) => MonadError e m
| m -> e where
#+END_SRC
This means that Haskell type system guarantees that for each
src_haskell{m} there exist unique src_haskell{e} if
src_haskell{MonadError e m} is inhabited. This, in turn, means that
substituting a constant src_haskell{Functor} src_haskell{r = \x a -> m a}
over src_haskell{Monad} src_haskell{m} into the definition of
src_haskell{ConjoinedMonads} produces
#+BEGIN_SRC haskell-spec
class ConjoinedMonads (\x a -> m a) where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
throw :: e -> m a
catch :: m a -> (e -> m a) -> m a
#+END_SRC
The first two operators are just the definition of src_haskell{Monad m},
the latter two match src_haskell{MonadError}'s src_haskell{throwError}
and src_haskell{catchError} exactly.
#+BEGIN_theorem
src_haskell{MonadError} is a src_haskell{ConjoinedMonads} that is constant
in its first index.
#+END_theorem
#+BEGIN_proof
By the above argument.
#+END_proof
** src_haskell{MonadThrow} and src_haskell{MonadCatch}
@@tex:\label{sec:instances:constant:monadcatch}@@
For src_haskell{MonadThrow} and src_haskell{MonadCatch}
(\cref{sec:monad-catch}) it is not the case that src_haskell{e} is
unique, since src_haskell{Exception e} is a whole class of types.
Moreover, operator src_haskell{catchM} of src_haskell{MonadCatch},
unlike src_haskell{catchError} of src_haskell{MonadError}, does
dynamic dispatch by src_haskell{cast}ing src_haskell{Exception}s to
the type of its handler's argument and propagating errors when the
src_haskell{cast} fails. Note that, strictly speaking, purely from
type perspective src_haskell{MonadCatch} is not /required/ but
/allowed/ to src_haskell{cast}, but all the instances do actually
src_haskell{cast}. The latter fact means that we can distill that
common computational pattern by redefining those structures using the
technique used by imprecise exceptions of \cref{sec:imprecise} as
follows
#+BEGIN_SRC haskell :tangle tng-main.hs
class Monad m => MonadThrowS m where
throwS :: SomeException -> m a
class MonadThrow m => MonadCatchS m where
catchS :: m a
-> (SomeException -> m a) -> m a
throwM' :: (MonadThrowS m, Exception e)
=> e -> m a
throwM' = throwS . toException
handleOrAgain h e = case fromException e of
Just f -> h f
Nothing -> throwM e
catchM' :: (MonadCatchS m, Exception e)
=> m a -> (e -> m a) -> m a
catchM' ma = catchS ma . handleOrAgain
#+END_SRC
Note that src_haskell{MonadCatchS} is, again, a constant
src_haskell{ConjoinedMonads} with error index fixed to
src_haskell{SomeException}.
Also note that src_haskell{throwM'} above is the only way to get an
equivalent for src_haskell{throwM} because src_haskell{toException} is
the only way to cast an arbitrary type to src_haskell{SomeException}.
On the other hand, src_haskell{catchM} from src_haskell{MonadCatch},
unlike src_haskell{catchM'} above, allows for instances that can
cheat. For example, src_haskell{catchM} can give a constant
src_haskell{SomeException} to the handler every time instead of
src_haskell{cast}ing anything. We feel that this implies that
src_haskell{MonadCatch} is not a proper formal structure for error
handling.
#+BEGIN_definition
@@tex:\label{dfn:proper-monad-catch}@@
**Proper src_haskell{MonadCatch} instance.** We shall call an
instance of src_haskell{MonadCatch} /proper/ when its
src_haskell{catchM} can be decomposed into src_haskell{catchS} and
src_haskell{handleOrAgain}.
#+END_definition
#+BEGIN_theorem
@@tex:\label{thm:instances:constant:monadcatch}@@
Every proper instance of src_haskell{MonadCatch} is a composition of
src_haskell{ConjoinedMonads} that is constant in its error index with
src_haskell{toException} in src_haskell{throwD} and
src_haskell{handleOrAgain} in src_haskell{catchD}. In particular,
src_haskell{MonadThrow} is a composition of src_haskell{Pointed} in
the error index with src_haskell{toException}.
#+END_theorem
#+BEGIN_proof
By the above reasoning.
#+END_proof
* Instances: parser combinators
@@tex:\label{sec:instances:parser-combinators}@@
In this section we discuss the application of src_haskell{ConjoinedMonads}
and \cref{dfn:proper} to src_haskell{Monad}ic parser combinators
discussed in \cref{sec:parser-combinators}.
** Inevitable definitions
To start off, let us continue using the definition of
src_haskell{Parser} type from
\cref{sec:parser-combinators:with-access}. The src_haskell{Monad}
instance in index src_haskell{e} for this type is similarly easy to
implement (by just trying all free functions of appropriate types) and
it, too, has two possible implementations
#+BEGIN_SRC haskell :tangle tng-main.hs
throwP :: e -> Parser s e a
throwP e = Parser $ \s -> Left (e, s)
catchP :: Parser s e a -> (e -> Parser s f a) -> Parser s f a
catchP p f = Parser $ \s ->
case runParser p s of
Right x -> Right x
Left (e, _) -> runParser (f e) s
catchP' :: Parser s e a -> (e -> Parser s f a) -> Parser s f a
catchP' p f = Parser $ \s ->
case runParser p s of
Right x -> Right x
Left (e, s') -> runParser (f e) s'
#+END_SRC
\noindent with src_haskell{catchP} doing backtracking on failures and
src_haskell{catchP'} proceeding to handling with the current state.
#+BEGIN_theorem
@@tex:\label{thm:instances:parser-combinators}@@
src_haskell{Parser} is a src_haskell{ConjoinedMonads} for both
versions of src_haskell{catchP}.
#+END_theorem
#+BEGIN_proof
src_haskell{Monad} laws for src_haskell{catchP'} follow from the
corresponding laws for src_haskell{(>>=)} of
\cref{sec:parser-combinators:with-access}.
The rest can be proven by trivial case analysis and/or by using the
observation from the proof of \cref{thm:with-heuristic}.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Let us also typecheck it
instance ConjoinedMonads (Parser s) where
creturn = return
cbind = (>>=)
cthrow = throwP
ccatch = catchP
#+END_SRC
#+END_proof
A curious consequence of the above theorem is that src_haskell{(>>=)}
of \cref{sec:parser-combinators:with-access} also has a roll-back
version which satisfies src_haskell{Monad} laws
#+BEGIN_SRC haskell :tangle tng-main.hs
bindP p f = Parser $ \s ->
case runParser p s of
Left x -> Left x
Right (a, _) -> runParser (f a) s
#+END_SRC
Though, of course, a src_haskell{Parser} that would use
src_haskell{bindP} in place of the usual src_haskell{(>>=)} could not
be called a "parser" anymore.
** The interesting parts
The first interesting fact is that src_haskell{(<|>)} operator of the
src_haskell{Alternative} (\cref{sec:alternative}) type class is simply
a type restricted version of src_haskell{orElseP} which, in turn, is
just src_haskell{(>>)} operator for the src_haskell{Monad} in index
src_haskell{e}
#+BEGIN_SRC haskell :tangle tng-main.hs
orElseP :: Parser s e a -> Parser s f a -> Parser s f a
orElseP f g = f `catchP` const g
#+END_SRC
#+BEGIN_SRC haskell-spec
instance Monoid e => Alternative (Parser s e) where
empty = Parser $ \s -> Left (mempty, s)
f <|> g = f `orElseP` g
#+END_SRC
Of even more interest is the fact that substituting
src_haskell{orElseP} instead of src_haskell{(<|>)} into the definition
of src_haskell{many} operator produces src_haskell{many} and
src_haskell{some} operators with types that show that
src_haskell{some} inherits error produced by its argument while
src_haskell{many} ignores them
#+BEGIN_SRC haskell :tangle tng-main.hs
someP :: Parser s e a -> Parser s e [a]
someP v = fmap (:) v <*> manyP v
manyP :: Parser s e a -> Parser s f [a]
manyP v = someP v `orElseP` pure []
#+END_SRC
This method of substituting src_haskell{(<|>)} with
src_haskell{orElseP} extends to other similar combinators like
src_haskell{choice}, src_haskell{optional}, src_haskell{notFollowedBy}
of all three aforementioned parser combinator libraries (Parser,
Attoparsec, Megaparsec) and similar structures. The overall effect of
this substitution is very useful in practice: it produces generic
parser combinators that can be used to express parsers that are
precise about errors they raise and handle. We can not emphasize this
fact enough.
All of the above results of this section trivially generalize to their
src_haskell{MonadTrans} versions as usual.
* Instances: conventional src_haskell{throw} and src_haskell{catch} via src_haskell{callCC}
@@tex:\label{sec:instances:throw-catch-cc}@@
It is well-known fact that Emacs LISP-style src_haskell{throw} and
src_haskell{catch} can be emulated with Scheme's src_scheme{call/cc}
and some mutable variables~\cite{CSE341:2004:Scheme:Continuations,
WikiBooks:Scheme:Continuations}. As a Haskell instance, Neil Mitchel
used the same technique translated to Haskell's src_scheme{IORef}s and
src_haskell{callCC} in for Shake build system~\cite{Mitchell:2014:CE,
Mitchell:GitHub:Shake} (however, at the time of writing Shake no
longer uses that code). In this section we shall demonstrate that a
structure with the same semantics can be implemented in pure Haskell
without the use of mutable variables. In all the cases, as usual,
C++/Java-style dynamic dispatch can be added on top using the same
src_haskell{cast}ing technique of sections~\ref{sec:imprecise}
and~\ref{sec:instances:constant:monadcatch}. Hence without the loss of
generality in this section we shall discuss only the
most-recent-handler case.
** Second-rank src_haskell{callCC}
Remember the definition of src_haskell{callCC} from \cref{sec:callcc}.
The underappreciated fact about that function is that its type is not
its most general type for its term. Note that variable $b$ in Peirce's
law
$$((a \to b) \to a) \to a$$
\noindent plays the same role as src_haskell{r} plays in the
definition of src_haskell{Cont}: it is a generalization of the
bottom $\bot$ constant. This, of course, means that we can
generalize Peirce's law to
$$((\forall b . a \to b) \to a) \to a$$
\noindent and, by repeating the derivation in \cref{sec:callcc},
give the following second-rank type for src_haskell{callCC}
#+BEGIN_SRC haskell :tangle tng-main.hs
callCCR2 :: ((forall b . a -> Cont r b) -> Cont r a) -> Cont r a
#+END_SRC
\noindent while keeping exactly the same implementation.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- same as before
callCCR2 f = Cont $ \c ->
runCont (f (\a -> Cont $ \_ -> c a)) c
#+END_SRC
** src_haskell{ThrowT} src_haskell{MonadTrans}former
Note that, in essence, src_haskell{catch} maintains a stack of handler
addresses and src_haskell{throw} simply src_assembly{jmp}s to the most
recent one. Emulation of exceptions with src_scheme{call/cc} works
similarly~\cite{CSE341:2004:Scheme:Continuations,
WikiBooks:Scheme:Continuations}. The main never explicitly stated
observation in that translation is that the type of the handler in the
type of
#+BEGIN_SRC haskell-spec
catch :: M -> (e -> M) -> M
#+END_SRC
\noindent matches the type of src_haskell{throw :: e -> M} and the
type of escape continuation when src_haskell{M} is
src_haskell{ContT r m b}. In other words, we can simply assign
#+BEGIN_SRC haskell :tangle tng-main.hs
type Handler r e m = forall b . e -> ContT r m b
#+END_SRC
\noindent to be to type of our handler and since
src_scheme{callCC} provides an escape continuation directly to its
argument src_haskell{catch} can simply save it and
src_haskell{throw} can simply take the most recent one and escape
into it
#+BEGIN_SRC haskell :tangle tng-main.hs
throwT :: e -> ThrowT r m e a
throwT e = ThrowT $ \currentThrow -> currentThrow e
#+END_SRC
Also note that since the stack src_haskell{catch} maintains stays
immutable between src_haskell{catch}es and each state of the stack is
bound to the computation argument of src_haskell{catch}, in principle,
we should be able to use a simple context (pure function,
src_haskell{Reader}) instead of a mutable variable as follows
#+BEGIN_SRC haskell-spec
type ThrowT r m e a =
ReaderT (Handler r e m) -- for saving last handler
(ContT r m) -- for callCC
a
#+END_SRC
\noindent which, after inlining all the definitions except pure
src_haskell{Cont} becomes
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype ThrowT r m e a = ThrowT
{ runThrowT :: (forall b . e -> Cont (m r) b)
-> Cont (m r) a }
#+END_SRC
Finally, since the escape continuation of delimited
src_haskell{callCC} escapes to the same address where the body of
src_haskell{callCC} normally returns, to emulate a single
src_haskell{catch} we need to chain two src_haskell{callCC}s as
follows
#+BEGIN_SRC haskell :tangle tng-main.hs
catchT :: ThrowT r m e a
-> (e -> ThrowT r m f a)
-> ThrowT r m f a
catchT m h = ThrowT $ \outerThrow ->
callCC $ \normalExit -> do
e <- callCCR2 $ \newThrow -> runThrowT m newThrow >>= normalExit
-- newThrow escapes here
runThrowT (h e) outerThrow
-- normalExit escapes here
#+END_SRC
Note that this expression requires our second-rank
src_haskell{callCCR2} since our src_haskell{Handler} is universally
quantified by the variable src_haskell{b}. However, if we fix
src_haskell{e} to a constant type then the conventional
src_haskell{callCC} will suffice.
Similarly to other uses of generalized Kolmogorov's translation we,
too, can hide src_haskell{r} parameter behind src_haskell{forall}
# NOTE: prettier
@@tex:\newpage@@
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype ThrowT' m e a = ThrowT'
{ runThrowT' :: forall r
. (forall b . e -> Cont (m r) b)
-> Cont (m r) a }
throwT' :: e -> ThrowT' m e a
catchT' :: ThrowT' m e a
-> (e -> ThrowT' m f a)
-> ThrowT' m f a
#+END_SRC
\noindent without any changes to the bodies of src_haskell{throw}
and src_haskell{catch}.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- both essentially the same
throwT' e = ThrowT' $ \currentThrow -> currentThrow e
catchT' m h = ThrowT' $ \outerThrow ->
callCC $ \normalExit -> do
e <- callCCR2 $ \newThrow -> runThrowT' m newThrow >>= normalExit
runThrowT' (h e) outerThrow
#+END_SRC
#+BEGIN_theorem
For src_haskell{Monad} src_haskell{m} and any src_haskell{r},
src_haskell{ThrowT r m} and src_haskell{ThrowT' m} are
src_haskell{ConjoinedMonads}s.
#+END_theorem
#+BEGIN_proof
For each index.
- In index src_haskell{a}: src_haskell{ThrowT} is a special case of
src_haskell{ReaderT} and src_haskell{Cont} and src_haskell{m} are
src_haskell{Monad}s.
- In index src_haskell{e}: by substitution of the above definitions
into the src_haskell{Monad} laws, since the definitions of
src_haskell{throwT} and src_haskell{throwT'} are, essentially,
identity functions.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Let us also typecheck it
-- Monad
instance Monad m => Pointed (ThrowT r m e) where
pure a = ThrowT $ \_ -> pure a
instance Monad m => Monad (ThrowT r m e) where
-- a lift of Cont's (>>=)
ma >>= f = ThrowT $ \err
-> Cont $ \c -> runCont (runThrowT ma err)
$ \a -> runCont (runThrowT (f a) err) c
instance Monad m => Pointed (ThrowT' m e) where
pure a = ThrowT' $ \_ -> pure a
instance Monad m => Monad (ThrowT' m e) where
-- copy-paste
ma >>= f = ThrowT' $ \err
-> Cont $ \c -> runCont (runThrowT' ma err)
$ \a -> runCont (runThrowT' (f a) err) c
-- Monadic boilerplate
instance Monad m => Functor (ThrowT r m e) where
fmap = liftM
instance Monad m => Applicative (ThrowT r m e) where
(<*>) = ap
instance Monad m => Functor (ThrowT' m e) where
fmap = liftM
instance Monad m => Applicative (ThrowT' m e) where
(<*>) = ap
-- The thing
instance (Monad m) => ConjoinedMonads (ThrowT r m) where
creturn = return
cbind = (>>=)
cthrow = throwT
ccatch = catchT
instance (Monad m) => ConjoinedMonads (ThrowT' m) where
creturn = return
cbind = (>>=)
cthrow = throwT'
ccatch = catchT'
#+END_SRC
#+END_proof
* Instances: error-explicit src_haskell{IO}
@@tex:\label{sec:instances:eio}@@
As we saw in \cref{sec:imprecise}, src_haskell{IO} is defined as a
src_haskell{State} src_haskell{Monad} with some magical primitive
operations.[fn::Some of which actually break src_haskell{Monad} laws,
but as mentioned in \cref{rem:io-caveats} that is out of scope of this
discussion.] Which means there is nothing preventing us from extending
that src_haskell{IO} signature with a type for errors.
#+BEGIN_SRC haskell-spec
newtype EIO e a
#+END_SRC
Similarly to parser combinators of
\cref{sec:instances:parser-combinators} there are several possible
implementations of this src_haskell{EIO} (including, in principle, the
ones that do backtracking on errors, though, of course, that would be
inconsistent with the semantics of the src_haskell{RealWorld}). The
simplest one matches a definition for non-backtracking parser
combinator on src_haskell{State# RealWorld} from
\cref{sec:parser-combinators:with-access}
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype EIO e a = EIO
{ runEIO :: State# RealWorld
-> (# Either e a, State# RealWorld #) }
instance Pointed (EIO e) where
pure a = EIO $ \s -> (# Right a, s #)
instance Monad (EIO e) where
m >>= f = EIO $ \s -> case runEIO m s of
(# Left a, s' #) -> (# Left a, s' #)
(# Right a, s' #) -> runEIO (f a) s'
-- Note how symmetric this is with Pointed and Monad instances.
throwEIO :: e -> EIO e a
throwEIO e = EIO $ \s -> (# Left e, s #)
catchEIO :: EIO e a -> (e -> EIO f a) -> EIO f a
catchEIO m f = EIO $ \s -> case runEIO m s of
(# Left a, s' #) -> runEIO (f a) s'
(# Right a, s' #) -> (# Right a, s' #)
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor (EIO e) where
fmap = liftM
instance Applicative (EIO e) where
(<*>) = ap
#+END_SRC
Note that very similar structures were proposed before
in~\cite{Iborra:2010:ETE} and
src_haskell{Control.Monad.Exception.Catch} module of
=control-monad-exception=~\cite{Hackage:control-monad-exception0112}
discussed in \cref{sec:other-monadic-generalizations}.
Also note that the definition of GHC's src_haskell{IO} before
imprecise exceptions were introduced was similar to src_haskell{EIO}
above (but without the parameter src_haskell{e}) and one of the
primary motivations behind introduction of builtin exceptions into GHC
mentioned in \cite{PeytonJones:1999:SIE} was to make src_haskell{IO}
more efficient by allowing its src_haskell{(>>=)} to be implemented
without pattern-matching. But there are, of course, other ways to
eliminate pattern matching. By moving src_haskell{Either} in the
definition of src_haskell{EIO} out the parentheses using the technique
from \cref{sec:parser-combinators:with-access} and then Scott-encoding
the resulting type we can make the following definition
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype SEIO e a = SEIO
{ runSEIO :: forall r
. (e -> State# RealWorld -> r)
-> (a -> State# RealWorld -> r)
-> State# RealWorld
-> r }
instance Pointed (SEIO e) where
pure a = SEIO $ \err ok s -> ok a s
instance Monad (SEIO e) where
m >>= f = SEIO $ \err ok s -> runSEIO m err (\a -> runSEIO (f a) err ok) s
-- Note the same here.
throwSEIO :: e -> SEIO e a
throwSEIO e = SEIO $ \err ok s -> err e s
catchSEIO :: SEIO e a -> (e -> SEIO f a) -> SEIO f a
catchSEIO m f = SEIO $ \err ok s -> runSEIO m (\e -> runSEIO (f e) err ok) ok s
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Functor (SEIO e) where
fmap = liftM
instance Applicative (SEIO e) where
(<*>) = ap
#+END_SRC
#+BEGIN_theorem
@@tex:\label{thm:instances:eio}@@
Both src_haskell{EIO} and src_haskell{SEIO} with the above
operations are src_haskell{ConjoinedMonads}s.
#+END_theorem
#+BEGIN_proof
Consequence of \cref{thm:instances:parser-combinators} and the fact
that Scott-encoding preserves computational properties.
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
-- Let us also typecheck it
instance ConjoinedMonads EIO where
creturn = return
cbind = (>>=)
cthrow = throwEIO
ccatch = catchEIO
instance ConjoinedMonads SEIO where
creturn = return
cbind = (>>=)
cthrow = throwSEIO
ccatch = catchSEIO
#+END_SRC
#+END_proof
* Instances: conventional src_haskell{IO}
@@tex:\label{sec:instances:io}@@
#+BEGIN_theorem
@@tex:\label{thm:instances:io}@@
src_haskell{IO} is a composition of src_haskell{ConjoinedMonads} that is
constant in its error index with src_haskell{toException} in
src_haskell{raiseIO#} and src_haskell{handleOrAgain} in
src_haskell{catch#}.
#+END_theorem
#+BEGIN_proof
A consequence of of results of
theorems~\ref{thm:instances:constant:monadcatch}
and~\ref{thm:instances:eio} for src_haskell{e == SomeException}.
#+END_proof
Note that, according to \cref{rem:io-caveats}, the above works out
only because src_haskell{raiseIO#}/src_haskell{throwIO}, unlike
src_haskell{raise#}/src_haskell{throw}, are deterministic (see
\cref{sec:imprecise}).
Also note that in a dialect of Haskell with separate operators for
imprecise exceptions (or without imprecise exceptions altogether) we
can completely replace src_haskell{IO} with src_haskell{EIO} as
defined above. We can not, however, apply that construction to GHC's
Haskell dialect since it merges precise and imprecise
src_haskell{catch} (see \cref{rem:io-two-kinds-of-exceptions}).
* Applicatives
@@tex:\label{sec:applicatives}@@
Now let us once more turn our attention to the bodies of
definitions~\ref{dfn:proper}, \ref{dfn:fishy},
and~\ref{dfn:proper-haskell} (all of which define the same structure).
#+BEGIN_SRC haskell-spec
class (forall a . Monad (\e -> m e a))
, forall e . Monad (m e)
=> ConjoinedMonads m where
#+END_SRC
Since src_haskell{ConjoinedMonads} is simply a
src_haskell{Monad}@@tex:~$\times$~@@src_haskell{Monad} with
interaction laws between src_haskell{pure} and src_haskell{bind}
operators (\cref{dfn:proper}) it is natural to ask what would happen
if we replace one or both of those src_haskell{Monad}s with more
general structures like src_haskell{Applicative} and modify the
interaction laws accordingly.
The two structures with src_haskell{Applicative} in index
src_haskell{e} seem to be unusable for the purposes of this article
since they lack conventional error handling operators. However, the
structure with src_haskell{Monad} in index src_haskell{e} and
src_haskell{Applicative} in index src_haskell{a} looks interesting.
#+BEGIN_SRC haskell-spec
class (forall a . Monad (\e -> m e a))
, forall e . Applicative (m e)
=> MonadXApplicative m where
#+END_SRC
In this structure the src_haskell{Monad}ic index gives conventional
src_haskell{throw} and src_haskell{catch} operators, and the
src_haskell{Applicative} index can be treated as expressing
generalized function application (see \cref{sec:applicative-functor})
for structure src_haskell{m}.
In other words, when the above structure preserves errors and
pure values similarly to \cref{dfn:proper}
#+BEGIN_SRC haskell-spec
throw e <*> a == throw e
pure a `catch` f == pure a
#+END_SRC
\noindent (and obeys the laws of src_haskell{Applicative} and
src_haskell{Monad} for corresponding operators) then it can be used
to express $\lambda$-calculus with exceptions by simply injecting
all src_haskell{pure} values and src_haskell{lift}ing all pure
functions into it.
In particular, since src_haskell{ConjoinedMonads} is a special case of
src_haskell{MonadXApplicative}, all src_haskell{ConjoinedMonads} instances
from the previous sections can be used as a basis for such a
formalism.
While it is not immediately clear how to make imprecise exceptions
into an instance of src_haskell{MonadXApplicative} (since they are
non-deterministic, hence disobeying the above laws, and
src_haskell{throw} having a wrong type to be the identity element for
src_haskell{catch}, see \cref{rem:io-two-kinds-of-exceptions}), there
are some interesting instances of src_haskell{MonadXApplicative} that
are not src_haskell{ConjoinedMonads}.
For instance, a folklore example of an src_haskell{Applicative} that
is not a src_haskell{Monad} is "computations collecting failures in a
src_haskell{Monoid}", which can be defined as follows
#+BEGIN_SRC haskell :tangle tng-main.hs
newtype EA e a = EA { runEA :: Either e a }
instance Pointed (EA e) where
pure = EA . Right
instance Monoid e => Applicative (EA e) where
f <*> a = EA $ runEA f <**> runEA a where
(Right f) <**> (Right a) = Right $ f a
(Right f) <**> (Left e) = Left e
(Left e) <**> (Right a) = Left e
(Left e1) <**> (Left e2) = Left $ e1 `mappend` e2
#+END_SRC
Note, however, that this structure is a src_haskell{Monad} in
src_haskell{e}
#+BEGIN_SRC haskell :tangle tng-main.hs
throwEA :: e -> EA e a
throwEA = EA . Left
catchEA :: EA e a -> (e -> EA f a) -> EA f a
(EA a) `catchEA` f = case a of
Right a -> pure a
Left e -> f e
#+END_SRC
#+BEGIN_SRC haskell :tangle tng-main.hs :exports none
instance Monoid e => Functor (EA e) where
fmap f a = pure f <*> a
#+END_SRC
\noindent which means it is also an instance of
src_haskell{MonadXApplicative}. If we now remember that
- graded monads~\cite{Katsumata:2014:PEM} also require src_haskell{e}
to be a src_haskell{Monoid} and
- imprecise exceptions, too, can be though as producing a
src_haskell{Monoid} of possible errors with src_haskell{catch}
(including the implicit src_haskell{catch} over src_haskell{main})
"observing" one of its elements,
\noindent we come to a conclusion that in a calculus with
src_haskell{IO}-effects separated from non-determinism-effects,
imprecise exceptions over non-deterministic src_haskell{Applicative}
computations, indeed, form a src_haskell{Monad} (with equivalence
defined up to raising the same set of exceptions, similarly to section
4 of~\cite{PeytonJones:1999:SIE}) over the src_haskell{Monoid} of
imprecise exceptions. That is, those, too, are examples of
src_haskell{MonadXApplicative}.
* Conclusions and future work
We hope that with this article we pointed and then at least partially
plugged an algebraic hole in the programming languages theory by
showing that conventional computational formalisms with
src_haskell{throw/try/catch}-exceptions are "conjoined" products of
pairs of src_haskell{Monad}s (or, less imperatively,
src_haskell{Monad}s and src_haskell{Applicative}s). This fact, in our
opinion, makes a lot of conventional programming "click into place"
similarly to how plain src_haskell{Monad}s "click" imperative
"semicolons".
Of particular note is the fact that everything in this paper,
including src_haskell{EIO} of \cref{sec:instances:eio}, follows the
"marriage" framework of~\cite{wadler-thiemann-03} of confining effects
to monads, but ignores the question of any additional rules for type
indexes in question. In other words, ad-hoc exception encoding
constructions like that of error-explicit IO~\cite{Iborra:2010:ETE} or
graded monads~\cite{Katsumata:2014:PEM} are mostly orthogonal to our
"conjoined" structures and can be used simultaneously.
Besides practical applications described in the body of the paper and
observations already mentioned in \cref{sec:extabstract} (rereading
said section about now is highly recommended) we also want turn your
attention to the following observations.
1. Conventional error handling with src_haskell{throw} and
src_haskell{catch} (but without dynamic dispatch) is dual to
conventional src_haskell{Monad}ic sequential computation, a fact
which, in our opinion, is interesting by itself (see
footnote~\ref{fn:its-dual}).
1. Meanwhile, the "without dynamic dispatch" part above, in our
opinion, provides an algebraic foundation for the argument against
building new languages with builtin dynamic dispatch of exception
handlers and/or an argument against extensively relying on that
feature in the languages that have it, a point which is commonly
discussed in the folklore ("exceptions are evil") and was
articulated by Hoare from programmer comprehension standpoint
already in 1981~\cite{Hoare:1981:EOC}. Not only dynamic dispatch of
exceptions is, citing Hoare, "dangerous", but it also prevents
programs from directly accessing the inherent src_haskell{Monad}ic
structures discussed in this article.
1. We feel that the usual arguments against using src_haskell{Monad}s
for error handling are moot.
- The problem of syntactic non-uniformness between pure
computations, src_haskell{Applicative}s and src_haskell{Monad}s,
in our view, is almost trivial to solve: common primitives like
src_haskell{map}/src_haskell{mapM} should be expressed in terms
of src_haskell{Applicative}s (of which pure functions are trivial
instance) instead of src_haskell{Monad}s. For instance,
src_haskell{mapM} for list[fn::And, similarly, for
src_haskell{Traversable} which we shall continue to ignore for
the purposes of this article.] can be rewritten as
#+BEGIN_SRC haskell :tangle tng-main.hs
mapAp :: Applicative f => (a -> f b) -> [a] -> f [b]
mapAp f [] = pure []
mapAp f (a:as) = fmap (:) (f a) <*> mapAp f as
#+END_SRC
Meanwhile, the uniform syntax for pure functions and
src_haskell{Applicative}s can be made by adding some more missing
instances of the LISP macros into the compiler in
question.[fn::From a cynical LISP-evangelist point of view, all
of "the progress" of the programming languages in the last 50
years can be summarized as "adopting more and more elements
(lately, meta-programming) from LISP while trying very hard
not to adopt the syntax of LISP". From a less cynical
perspective, "the progress", at least in typed languages,
consists of well-typing said elements.] For instance,
quasiquotation~\cite{Mainland:2007:WNQ} is one conventional way
do such a translation, Conal Elliot's "Compiling to
Categories"~\cite{Elliott:2017:CTC} provides another
categorically cute way to achieve similar results.
- We feel that the problem of modularity as stated by
Brady~\cite{Brady:2013:PRA}
#+BEGIN_QUOTE
Unfortunately, useful as monads are, they do not compose very
well. Monad transformers can quickly become unwieldy when
there are lots of effects to manage, leading to a temptation in
larger programs to combine everything into one coarse-grained
state and exception monad.
#+END_QUOTE
can be solved by applying graded monads to the src_haskell{Monad}
part of src_haskell{MonadXApplicative}.
In other words, we think that a programming language that
- provides a primitive src_haskell{catch} operator that does no
dynamic dispatch,
- provides quasi-quoting/compiling to categories for
src_haskell{Applicative}s,
- distinguishes between src_haskell{IO}-effects and non-determinism,
and
- uses a graded src_haskell{MonadXApplicative} for a base type of
computations
\noindent would provide all the efficiency of imprecise exceptions,
simplicity of src_haskell{Monad}s (doubled, in some sense, since error
handling would stop being special), while having none of the
usual arguments against said mechanisms applying to it.
We feel that the following future work directions on the topic would
be of particular value:
- implementation of a practical "good-enough" (\cref{sec:encodings})
library for GHC Haskell, and, eventually, an implementation of a
dialect of Haskell with a graded src_haskell{MonadXApplicative} as a
base type of computations,
- research into syntax and semantics of "marriages" between precise
and imprecise exceptions in a single language, including, but not
limited to, research into simpler semantic models for
$\lambda$-calculus with Monads~\cite{wadler-thiemann-03,
Filinski:1994:RM},
- research into the question of whether multiplying more than two
src_haskell{Monad}s and src_haskell{Applicatives} with non-trivial
interaction laws produces interesting structures.[fn::It is clear
that one can have more than one index src_haskell{e} conjoined to a
single src_haskell{a}, but such a construction doesn't seem to make
much sense in presence of graded src_haskell{Monad}s. However, that
fact by itself does not exclude a possibility of existence of an
interesting structure for which there are non-trivial interactions
between different indexes src_haskell{e}.]
All the practical results of this article except for
src_haskell{catchT} combinator of \cref{sec:instances:throw-catch-cc}
were born in 2014 in a course of a single week from observing the
structure of a parser combinator src_haskell{Monad} indexed by errors
and values (and other things beyond the scope of this article, the
original structure is also an indexed src_haskell{State}
src_haskell{Monad} to allow parsing of arbitrary data types, not just
streams) a very simplified version of which was presented in
\cref{sec:parser-combinators,sec:instances:parser-combinators}. The
article itself was started in 2016 but then was rewritten from scratch
four times before finally settling to the current presentation. The
src_haskell{catchT} combinator was discovered while writing
\cref{sec:continuations}.
This article would have been impossible without the patience of Sergei
Soloviev who read and meticulously commented numerous drafts of the
paper, numerous people who encouraged me to write this after I
described the general idea to them, and all contributors to Emacs and
org-mode without whom neither the planning nor the writing of the
actual text would have been manageable. The author is also grateful to
@@tex:\fbox{Sergey Baranov}@@ for helpful discussions on related
topics which steered the first half of this paper into its current
form.