#+TITLE: On the Expressive Power of Indexed Applicative and Monadic Structures
#+AUTHOR: Jan Malakhovski
#+EMAIL: papers@oxij.org
#+EMAIL-COMMENT: preferably with "thesis" as a substring of the subject line
#+AFFIL: IRIT, University of Toulouse-3 and ITMO University
#+DATE: October 25, 2019
#+VERSION: 1.1
#+KEYWORDS: applicative functors, monads, indexed monads, algebraic data types, metaprogramming, stack machines, parser combinators, logic, category theory
#+OPTIONS: H:5
@@tex:\newcounter{dummy}\refstepcounter{dummy}@@
#+BEGIN_abstract
@@tex:\label{sec:abstract}@@
It is well-known that very simple theoretic constructs such as src_haskell{Either} (type-theoretic equivalent of the logical "or" operator), src_haskell{State} (composable state transformers), src_haskell{Applicative} (generalized function application), and src_haskell{Monad} (generalized sequential program composition) structures (as they are named in Haskell) cover a huge chunk of what is usually needed to elegantly express most computational idioms used in conventional programs.
However, it is conventionally argued that there are several classes of commonly used idioms that do not fit well within those structures, the most notable examples being transformations between trees (data types, which are usually argued to require ether generalized pattern matching or heavy metaprogramming infrastructure) and exception handling (which are usually argued to require special language and run-time support).
This work aims to show that many of those idioms can, in fact, be expressed by reusing those well-known structures with minor (if any) modifications.
In other words, the purpose of this work is to apply the KISS (Keep It Stupid Simple) and/or Occam's razor principles to algebraic structures used to solve common programming problems.
@@tex:\vspace{1cm}@@
Technically speaking, this work aims to show that natural generalizations of src_haskell{Applicative} and src_haskell{Monad} type classes of Haskell combined with the ability to make Cartesian products of them produce a very simple common framework for expressing many practically useful things, some of the instances of which are very convenient novel ways to express common programming ideas, while others are usually classified as effect systems.
On that latter point, if one is to generalize the presented instances into an approach to design of effect systems in general, then the overall structure of such an approach can be thought of as being an almost syntactic framework which allows different effect systems adhering to the general structure of the "marriage" framework~\cite{wadler-thiemann-03} to be expressed on top of.
(Though, this work does not go into too much into the latter, since this work is mainly motivated by examples that can be immediately applied to Haskell practice.)
Note, however, that, after the fact, these technical observation are completely unsurprising: src_haskell{Applicative} and src_haskell{Monad} are generalizations of functional and linear program compositions respectively, so, naturally, Cartesian products of these two structures ought to cover a lot of what programs usually do.
@@tex:\vspace{1cm}@@
Unless you are reading the document you yourself recently fetched from https://oxij.org/thesis/PhD/ there is likely to be a better version of this document there.
It is not too late to switch to reading that one yet.
#+END_abstract
#+BEGIN_EXPORT tex
\chapter*{Acknowledgments}
#+END_EXPORT
This work would have been impossible without Sergei Soloviev who patiently read and meticulously commented numerous drafts of this document, generously gave invaluable advice, encouraged me to pursue ideas I was ready to discard, spent weeks of his netto-time discussing topics in science, literature, politics, and other facets of intellectual life with me, and helped me to carry through numerous bureaucratic hurdles.
These four years of close work with Sergei thoroughly demonstrated to me what "scientific advisor" actually meant to mean and even managed to soften my general outlook on academic life when I thought I was completely disillusioned.
This work would have also been impossible without numerous people, including but not limited to @@tex:\fbox{Sergey Baranov}@@, Nikolay Vasilyev, Georgiy Korneev, Ralph Matthes, Maxim Buzdalov, Alexey Sergushichev, and Anatoly Shalyto, who encouraged me to pursue these topics after I described the general ideas to them.
Of those, discussions with Georgiy Korneev and Sergey Baranov were of most tremendous help and influence: discussions with Georgiy convinced me to pursue these topics in the first place, while discussions on related topics and critiques of ideas presented in this work by Sergey steered the first half of this document into its current form.
I also want to thank Thomas Ehrhard and Christian RetorĂ© for their helpful feedback that pointed to the parts of the manuscript that needed further clarifications and emphasis.
#+BEGIN_EXPORT tex
\begin{center}
$\star$
\end{center}
#+END_EXPORT
There are numerous people whose efforts produced intellectual environments that steered my general thought patterns into their current states.
For most of them I won't ever know their names, nor the degree to which their work and/or ideas influenced me, but there are some I can immediately remember:
- developers and contributors to GHC Haskell compiler, Coq, Agda, and, most recently, Idris and Lean theorem provers, their underlying calculi, as well as their numerous libraries, whose monumental efforts created tools that allowed computers to be taught enough mathematics and algebra for them to teach it back to me, who started as an undergraduate uninterested in anything but the most "practical" of computing;
- developers and contributors to Emacs and Org-Mode without whom neither the planning, nor the writing of the actual text of this document, nor the steering of the rest of my intellectual life would have been manageable;
- developers and contributors to NixOS and sibling projects without whom I would have gone insane managing my computing devices;
- Aleksandr Lubischev, Daniel Dennett, Noam Chomsky, Scott Aaronson, and Eliezer Yudkowsky whose numerous works on self-discipline, philosophy, rationality, numerous pointers to other fascinating literature, and, for the latter author, even his fictional stories, formed my recent years (I wish I started reading those things when I was nine).
#+BEGIN_EXPORT tex
\begin{center}
$\star$
\end{center}
#+END_EXPORT
Last but not least, I want to thank my family that supports me regardless of anything I do.
#+BEGIN_EXPORT tex
\chapter*{To the Reader}
#+END_EXPORT
Historiography (a set of, usually documented, events) in general, and the historiography of programming languages in particular, is rather messy.
Any attempt at making it into a /history/, that is, a story, necessarily means selecting a starting point, throwing most of the relevant events out and then smoothing transitions between rather discrete points that are still left as to make the whole look a set of interwoven continuous streams following some internal or external logic, the most popular choice being causality.[fn::
As a fun example, Brownian motion was described by Lucretius in his scientific poem "On the Nature of Things" circa 60 BCE, and Nobel prize in physics for works about this phenomenon was awarded to Jean Perrin in 1926.
Which is not to say that either contribution or any of the unknown preceding and known intermediate events that were ignored in the previous sentence are inconsequential (in fact, on the contrary, anything of consequence is usually independently rediscovered at least twice, which itself can be used as a metric of importance of results in a particular work), but to say that history of physics of matter presented as a smooth sequence of discoveries is pure fiction.]
In regards to literary scientific works this process requires supplying them with historical introductions and organizing new discoveries to be presented in some "logical" fashion to make the work in question look as a nice logically consistent extension of those historical accounts.
However, it is important to remember that the reality of both historiography of things preceding a given work and historiography of discoveries described in it is often just a set of accidents.
Which is to say that history in general, and presentation of results of a given work in particular, is fiction whose only purpose is to confuse reader's mind to redirect his/her attention from inconvenient messy facts to convenient seemingly logically consistent stories of a kind that is easy to retain in human memory.[fn::
Which, by the way, is also very much the case for autobiographic history and thus self-authoring part of what is usually called "personality".
But we digress.]
Or, as they say, "stories trump data".
This work, being a Ph.D. thesis, shall follow the tradition and amply spice up the technical results with those fictional accounts.
However, the author boldly assumes that there are readers uninterested all these fictional wrappers some of whom are also convinced that a programming language like Haskell and/or its libraries can not be learned by reading a document without doing any actual programming practice.
Such readers might be interested in the following facts.
- Firstly, note that this work uses Haskell syntax extensively for the purposes of precise expression of thought.
In particular, most proofs use Haskell notation for equation reasoning and normal descriptive text uses Haskell type class names for the names of the respective algebraic structures where appropriate (e.g. "src_haskell{Monad}" instead of "monad").
- Secondly, assuming some familiarity with Haskell, this work can be read by starting from the \hyperref[sec:abstract]{abstract} above, followed by \cref{sec:prelude}, followed by jumping to the "meat" of the matters by following the intra-document hyperlinks of \cref{sec:contributions}.
Following this regime effectively cuts the number of pages in this work in half.
Note, however, that the document organized in such a way so that one could seamlessly fallback to the basics in case some algebraic structure is not familiar by following links to sections of \cref{sec:not-tutorial:basic} and \cref{sec:not-tutorial:non-basic} on by-need basis.
Anything lacking there can usually be answered by referencing Diehl's web-page~\cite{Diehl:2016:WIW}, GHC's =base= package~\cite{Hackage:base4900}, especially the types and descriptions of functions from the src_haskell{Prelude} module, and Typeclassopedia~\cite{HaskellWiki:Typeclassopedia}.
- Thirdly, this work is organized as a series of Literate Haskell programs in a single Emacs Org-Mode tree~\cite{OrgMode,Schulte:2011:MLCELPRR} (then, most likely, compiled into the representation you are looking at right now).
The literate source itself is available at [[https://oxij.org/thesis/PhD/]] and embedded straight into the PDF version of this work (click \attachfile{thesis.org} or look for "attachments" in your PDF viewer).
In author's opinion, technical details of sections involving Scott-encoded data types and CPS-transformed terms are incomprehensible without some hacking (playing, experimenting) with terms and types of the Literate version loaded into =ghci=.
The two most essential techniques for interacting with =ghci= employed by the author himself are:
- replacing random terms in the source with "src_haskell{_}" holes, reloading, and looking at compiler output, and
- erasing and then trying to interactively reinvent the terms in question using "src_haskell{_}" holes.
All runnable sources were tested with GHC~\cite{GHC} version 8.6.
# The tangled sources can be extracted via
# $ emacs --batch --eval "(progn (require 'ob-tangle) (org-babel-tangle-file \"thesis.org\"))"
# or by openining this file in Emacs and running `M-x org-babel-tangle`.
- Finally, the honest account of the historiography of this work is as follows.
All of the results presented in this work are either side-effects of conscious efforts to reuse algebraic structures of author's liking to solve author's common programming problems or things accidentally discovered while trying to explain those efforts in talking or writing.
Everything else, including the presented sequencing from simpler to more complex algebraic structures and the story and the overall philosophical picture of where this work falls within modern programming practice and language design are after-the-fact fictions.
For other readers, let us note that this work is written in such a way so that familiarity with Haskell (or even $\lambda$-calculus) is not actually required to understand the outline of ideas this work presents.
The minimal effective dose of Haskell (and $\lambda$-calculus) can be learned by osmosis by reading this work in a linear fashion.
Moreover, we are obliged to specifically point out that despite the heavy use of Haskell notation, most of the results of this work are actually **language-agnostic** and can be applied (if not straight to practice, then at least to inform design choices) to almost any programming language.
#+BEGIN_EXPORT tex
\small\tableofcontents\normalsize
#+END_EXPORT
* Introductions
** General Introduction
First programmable computers like Colossus (1943-1945) and even the early revisions of ENIAC (1945-1955) were not stored-program computers and could only be programmed using plugboards and mechanical switches.
IBM 650 (1953-1969), the first mass-produced computer, used a magnetic drum as its memory (usually initially loaded from punch-cards) and each instruction's operation code (opcode) had to explicitly specify the address of the next instruction (similarly to how src_assembly{jump} instructions of modern Assembly languages do).
The first computer with proper hardware support for subroutine calls of non-fixed-level nesting depth (that is, supporting recursion and arbitrary modularity) seems to be the PDP-11 (1970-1990), even though the support for simple subroutines was present even on the early ENIAC.
What these early examples show is that the very concept of a mostly linear program organized using modular possibly recursive subroutines had no hardware support until 1970s.
Most interestingly, however, as soon as those things got hardware support, the UNIX and the C programming language~\cite{Johnson:1973:PLB,Ritchie:1973:UTSa,Kernighan:1978:CPL} were born.
Both mostly equivalent hardware and those software systems are still ubiquitous even today.
(One could argue that the only big change in the commonly employed computer architecture since 1970s is the popularization of SIMD for numerical computations.
That is, the fact that almost all consumer-facing computers now come with GPUs out-of-the box.
There is also a revival of hardware virtualization, first introduced on IBM System/370 in 1972 and then forgotten until mid-2000s, but both hardware support for arbitrarily nested virtualization and software use of those features, a good contemporary example of which would be QubesOS~\cite{QubesOS}, are still rather lacking at the moment of writing of this work.)
The history of high-level programming languages starts with FORTRAN initially developed by John Backus at IBM (a compiler for IBM 704) around 1956 (first compiler delivered in 1957) and LISP initially developed by John McCarthy at MIT around the same time (first specified in 1958, first universal interpreter implemented by Steve Russell for IBM 704 around 1960, first compiler written in LISP in 1962).
FORTRAN family of imperative compiled strictly-typed languages, including ALGOL, C and their descendants can be viewed as, at first, straightforward attempts to make a universal Assembly language, with later horizontal-gene-transfer/incorporation of structured programming constructs such as =if-then-else= statements, loops (both FORTRAN 77), arrays, modules (both Fortran 90, the later is also C++20), sometimes mixed with some object-oriented constructs from Simula (of which C++ is the prime example), and, after 50-odd years, ideas from functional programming (C++11 and later).
LISP family of functional interpreted dynamically-typed languages, by contrast, was going the other direction by starting from $\lambda$-calculus developed by Alonzo Church and his students in 1930s and 1940s with the explicit goal of making a minimalist universal computational formalism~\cite{Cardone:2006:HLC,Barendregt:1997:ILC} and building on top.
For the purposes of this discussion two most important features of LISP were the ability to /declare/ new language constructs using so called "special forms" (which were, effectively, partially lazy functions in an language with eager evaluation) and the ability to describe its own programs (reflection).
The latter property meant that runtime code generation and meta-programming were easy, and, even more importantly, the language could trivially interpret itself, thus allowing arbitrary extensions.
The end result is that most variants of LISP to this day can evaluate each other's terms.
Various mixes of the two approaches appeared over the years.
Two noteworthy families are
- imperative (usually) interpreted dynamically-typed languages starting with Smalltalk and represented by modern Python, Ruby, JavaScript, among others; and
- functional (usually) compiled statically-typed languages starting with ML and represented by modern OCaml, SML, and Haskell, among others.
Among those, the sequence of languages LISP \to ML \to Miranda \to Haskell is rather interesting because the step from LISP to ML replaced dynamic typing with a polymorphic type system and infix syntax at the cost of loosing both special forms and reflection, the step to Miranda switched to lazy evaluation by default (thus giving most of what special forms did), and the step to Haskell added type classes (thus giving a lot of what dynamic types did) and reintroduced reflection, among many other things.
In other words, Haskell was designed to conveniently express things commonly discussed in Programming Languages Theory (PLT) as its terms look similar to those used in school-level mathematics, strictly-typedness allows (but not guarantees) it to be efficient, and it has enough pieces of LISP and more powerful type systems (like dependent types) to express (or at least hint at how they could be expressed) concepts applicable to whole swaths of programming languages.
And indeed, most of the literature cited in this work uses Haskell or a variant of ML.
Haskell is also surprisingly popular for an "academic" language consistently staying in Top-50 of TIOBE Index~\cite{TIOBEIndex} (measures search requests), with its the most popular public code repository of Hackage~\cite{Hackage} listing over 5000 packages.
As a side note, the usual way to explain why imperative languages (like FORTRAN, ALGOL, C) "won" over LISP is to note that the latter required too many transistors to evaluate at agreeable speeds.
Where FORTRAN emitted a single Assembly src_assembly{add}, LISP-machine needed a whole lot of run-time type checking.
Then, the resurgence of popularity of Smalltalk descendants like Python, Ruby, JavaScript in late 1990s and early 2000s can be explained by, on the one hand, their general semantic similarity to FORTRAN descendants but with higher levels of programmer satisfaction (simpler syntax without explicit type signatures, automatic memory management, etc), and, on the other hand, the rise of the number of transistors available on an average consumer CPU, followed by the advent of just-in-time (JIT) compilation.
Though, note that most high-performance code for systems written in those languages is still implemented in C and FORTRAN to be called by said interpreters via foreign function interface (FFI).
For instance, NumPy~\cite{NumPy}, a Python library for high-performance numerical computations (and probably /the/ most well-known Python library in academic circles), is a Pythonic wrapper over a bunch of C (and some FORTRAN, translated into C) code.
The resurgence of interest in the functional programming in the later half of 2000s, on the other hand, comes with the advent of compilation techniques which made them usable in high-performance software systems.
Among other things, this allows some of those languages to produce complete or almost complete full-stack mono-language systems.
For instance, MirageOS project~\cite{MirageOS}, a modular operating system written entirely in ML.
Similarly, Go~\cite{GoLang:pkgs}, Haskell~\cite{Hackage:base4900}, and Rust~\cite{RustLang:std} standard libraries also try to limit their use of FFIs.
Which, of course, can be seen as either a good thing ("Yay! Readable code in a sane safe language!") when compared to languages that use a lot of C FFIs in their standard libraries (e.g. Python) or a bad thing ("Uhg! Now every language infrastructure reimplements everything from scratch!").
Note, however, that conventional CPUs are, essentially, interpreters for machine code (sequences of opcodes) compiled into hardware (the metal traces and semiconductor gates of which are then "interpreted" by the physical laws of electromagnetism).
Which is why languages that are closer to Assembly are easier to compile in such a way that semantically efficient source language programs are compiled into opcode programs that are efficient to evaluate on those machines.
GPUs discussed above, first marketed as "graphical accelerators", are now considered an essential piece of modern computing machinery, making modern image rendering and processing techniques, among other things, practically viable.
Therefore, it would be interesting to see software systems developed specifically for computers with "FPGA accelerators", since graph reductions performed by interpreters of functional programming languages can be made much more efficient on such machines (e.g., see Reduceron~\cite{ReduceronHomepage,Naylor:2012:RRR} project).
That is to say, it is not entirely obvious that FORTRAN descendants would still be "winning" on the computer systems running in the not so far future, as programs for computers with reversible computations (like raw electromagnetism and quantum computers) are very much functional~\cite{Sabry:2011:RQC,Altenkirch:2005:FQPL}, thus it might be both more efficient and cognitively simpler to implement those systems in functional languages from top to bottom.
In any case, this work deals with somewhat more conventional computations.
The main algebraic structures discussed in this work are src_haskell{Monads} introduced to functional programming from Category theory by Moggi~\cite{moggi-89, moggi-91} and popularized by Wadler~\cite{Wadler:1992:EFP} and src_haskell{Applicative} src_haskell{Functor}s introduced by McBride and Paterson~\cite{mcbride-paterson-08}.
These two structures can be seen as a straightforward generalizations of linear and functional program compositions respectively, that is, generalizations of the "semicolon" and "function call" operators.
To explain those generalizations, however, we need to start talking in Haskell.
** Short Introduction to Haskell
*** Term Notation
Firstly, to shortly explain Haskell term notation, let us consider school-level arithmetical expressions such as
$$a\ sin(2 \alpha) + b\ cos(\alpha) + mod(n, m)$$
Haskell notation, essentially, is a modification of plain-text arithmetical notation that requires all operators except the function call operator to be explicit, does not require parentheses around function calls and arguments, and does not separate them with commas.
In other words, in Haskell, multiplication of src_haskell{a} and src_haskell{b} can be written as src_haskell{a * b} while the expression src_haskell{a b} would denote an application of the argument "src_haskell{b}" to the function "src_haskell{a}", that is, a function call.
Thus, the most straightforward translation of the above expression into Haskell notation would look as follows
#+BEGIN_SRC haskell-spec
a * sin (2 * alpha) + b * cos alpha + mod n m
#+END_SRC
Note, however, that this means that in Haskell some expressions will have parentheses in somewhat unexpected places.
For instance, conventionally notated
$$mod(n, m + n)$$
\noindent becomes
#+BEGIN_SRC haskell-spec
mod n (m + n)
#+END_SRC
\noindent as src_haskell{mod n m + n} would be parsed as src_haskell{(mod n m) + n} since term juxtaposition, which denotes argument application, grammatically binds more strongly than anything else.
(The reader might feel these conventions to be an instance of useless non-conformism, but they actually make a lot of sense for a functional programming language where most programs spends most of their code doing function calls, as opposed to assigning results of computations of expressions to variables like most imperative languages do.)
Then, Haskell allows to make infix functions like src_haskell{(+)} into prefix functions by wrapping them into parentheses and the reverse by wrapping them with =`= symbols.
For instance, the above school-level term notation example can also be rewritten as
#+BEGIN_SRC haskell-spec
(+) (a * sin (2 * alpha)) (b * cos alpha) + n `mod` m
#+END_SRC
Finally, both constant variables and function declarations can be made by simply defining them in blocks of src_haskell{f a_1 a_2 ... a_n = b} expressions starting at the same indent, with src_haskell{f} denoting definition's name, src_haskell{a_1 ... a_n} denoting the names of its arguments (zero for constant variable and one or more for a function), and src_haskell{b} denoting a "function body", i.e. a term the expression in question should evaluate to when supplied with values for all of the arguments.
Let us consider, for instance, the following set of definitions
#+BEGIN_SRC haskell-spec
x = 2
y = 3
id z = z
foo c
= c * x + y
bar a b =
a * foo b
#+END_SRC
\noindent Such expressions should be read as left-to-right rewrite rules.
For example,
- src_haskell{x = 2} above says "in an expression, all instances of src_haskell{x} should be replaced with src_haskell{2}",
- and src_haskell{foo c = c * x + y} above says "in an expression, all instances of src_haskell{foo c} should be replaced with src_haskell{c * x + y} for all values of src_haskell{c}".
For instance, under the above definitions, the expression
#+BEGIN_SRC haskell-spec
x + foo 10
#+END_SRC
\noindent can be reduced to
#+BEGIN_SRC haskell-spec
2 + 10 * 2 + 3
#+END_SRC
\noindent which can then be reduced further by applying reduction rules for src_haskell{(+)} and src_haskell{(*)} operators.
Similarly, the whole set of the five definitions above, assuming src_haskell{x}, src_haskell{y}, and src_haskell{id} are not used anywhere else, can be reduced to
#+BEGIN_SRC haskell-spec
foo c = c * 2 + 3
bar a b = a * foo b
#+END_SRC
Moreover, function definition can also be inlined by using "$\lambda$-expression" notation from $\lambda$-calculus~\cite{barendregt}
#+BEGIN_SRC haskell-spec
bar a b = a * (\c -> c * 2 + 3) b
#+END_SRC
\noindent where src_haskell{\a_1 ... a_n -> b} denotes an anonymous (unnamed) function with an arguments src_haskell{a_1 ... a_n} and term src_haskell{b} as the body.
Thus, the normal src_haskell{f a_1 ... a_n = b} block notation can be viewed as a syntax sugar for src_haskell{f = \a_1 ... a_n -> b} blocks.
This, of course, means that Haskell can trivially provide a mechanism for "incomplete function calls" (also known as /currying/), that is, give simple semantics to expressions that call functions with some of their arguments missing by simply wrapping them with $\lambda$-expressions.
For instance,
#+BEGIN_SRC haskell-spec
z = bar 2
#+END_SRC
\noindent is equivalent to
#+BEGIN_SRC haskell-spec
z = (\b -> bar 2 b)
#+END_SRC
\noindent (in the theory of $\lambda$-calculus this transformation is called "$\eta$-expansion" and its reverse "$\eta$-reduction") which can then be reduced to
#+BEGIN_SRC haskell-spec
z = \b -> 2 * (\c -> c * 2 + 3) b
#+END_SRC
Then, function definitions can also use /pattern matching/ syntax, by spelling out the possible combinations of argument values.
For instance,
#+BEGIN_SRC haskell-spec
lnot 0 = 1
lnot 1 = 0
natMinus 0 = 0
natMinus n = n - 1
#+END_SRC
Outside of function definitions the same thing can also be written using the src_haskell{case} syntax construct, e.g.
#+BEGIN_SRC haskell-spec
lnot' x = case x of
0 -> 1
1 -> 0
#+END_SRC
Finally, there is also a builtin =if-then-else= construct
#+BEGIN_SRC haskell-spec
lnot'' x = if x == 0 then 1
else if x == 1 then 0
else -1
#+END_SRC
Note that the above description of the notation implies that all expressions in Haskell are referentially transparent (i.e. there's no distinction between "value" and "reference" types, everything is a value) and all functions are pure (i.e. without side-effects).
Thus, the act of evaluating a given Haskell expression (term) consists of repeated inlinings of all the definitions the term uses followed by repeated substitutions of applied function arguments into the corresponding function bodies (possibly with introductions of some intermediate $\lambda$-expressions) until nothing else can be reduced.
Therefore, working with "references" requires separate mechanisms, which we are going to discuss in the following sections.
Meanwhile, note that if one wants to evaluate a single term of a Haskell program (when compiling a Haskell program into machine code such a term named src_haskell{main}) then it and the rest of the program can be equivalently expressed as a bunch of nested $\lambda$-expressions and applications.
For instance, the five definitions above, when evaluating term src_haskell{bar}, can be equivalently expressed as
#+BEGIN_SRC haskell-spec
(\x \y ->
(\foo -> \a b -> a * foo b) (\c -> c * x + y)
) 2 3
#+END_SRC
In other words, when working with a single expression, named definitions given on separate lines can be viewed as a syntax sugar for a $\lambda$-expression introducing the name as an argument immediately followed by application of the body of that definition to that $\lambda$-expression.
Thus, the model of evaluation of Haskell expressions can be simplified even more: all Haskell does is it de-syntax-sugars its terms into something very similar to $\lambda$-calculus and then repeatedly substitutes function arguments into anonymous functions until nothing else can be reduced, i.e. this is exactly $\beta$-reduction of $\lambda$-calculus.
Note, however, that when dealing with function arguments, in Haskell, as in any other sane programming language, variables are never "captured".
For instance,
#+BEGIN_SRC haskell-spec
a = 2
foo x = a * x
bar a b = foo a * b
#+END_SRC
\noindent can be reduced to
#+BEGIN_SRC haskell-spec
bar a b = (2 * a) * b
#+END_SRC
\noindent not src_haskell{bar a b = a * a * b}, nor src_haskell{bar a b = 2 * 2 * b}, nor anything else.
That is to say, arguments of both named and anonymous functions can be freely renamed without changing the meaning of an expression, and hence proper definition of inlining and function argument substitution should respect that property.
Technically speaking, one can simply forget about variable names and consider variable references to be pointers to the corresponding function arguments, with a variable reference denoting a pointer to the closest enclosing argument with the same name introduced by a $\lambda$-expression.
Or, equivalently, one can annotate $\lambda$-expressions with numbers of variables they introduce (instead of their names) and make variable references into expressions denoting "an argument number $n$ of the @@tex:$m$'s@@ enclosing $\lambda$-expression".
Such an encoding bears a name of de Bruijn indicies~\cite{de-bruijn-72}.
Finally, we have to discuss recursive functions.
The simplest way to explain them is to think them as being non-inlineable and calling themselves using function pointers (which is essentially what compilation from Haskell to machine code does).
Alternatively, one can imagine that Haskell has a builtin fixed-point operator, which we could define as having the following rewrite rule
#+BEGIN_SRC haskell-spec
fix f = f (fix f)
#+END_SRC
\noindent and then to think of all recursive functions as using src_haskell{fix} while taking themselves (i.e. a pointer to themselves) as their first argument.
For instance,
#+BEGIN_SRC haskell-spec
fib' fib 0 = 1
fib' fib n = n + fib (n - 1)
fib = fix fib'
#+END_SRC
As a side note, note that the above shows that, basically, any pure Haskell program can be expressed in terms of just $\lambda$-expressions, src_haskell{fix}, and some primitive types (like integers) and their operators like src_haskell{(+)}.
The beauty of the untyped $\lambda$-calculus comes from the fact that it can also express src_haskell{fix} (and other fixed point operators), numbers, trees, operators over them, and, in fact, anything computable, using cleverly constructed $\lambda$-terms and nothing else.
That is, untyped $\lambda$-calculus is a truly minimalist universal programming language.
A reader interested in such things is referred to~\cite{barendregt,Barendregt:1991:TPS}.
Visitors from the outer space culturally unrelated to the human race are very unlikely to know anything about x86 assembly (unless they specifically tried to learn it), alien races anatomically dissimilar to humans might even not know about Turing machines (since a Turing machine does not make much sense unless you are accustomed to manipulating your own hands), but they will probably know about prime numbers and $\lambda$-calculus (in the de Bruijn form).
*** Type Notation
In theory, Haskell is a strictly typed language and, hence, a programmer coming from an imperative language would probably expect to see a lot of type annotations.
In practice, however, one can write a lot of Haskell code without ever mentioning types.
Since Haskell supports type inference almost all type annotations can usually be left out.
However, spelling out the types of expressions can be useful for documentation and debugging purposes, it is also required in some syntactic expressions, like data types and type classes discussed below.
In plain Haskell 98, to attach a type to an expression one uses src_haskell{a :: t} syntax, where src_haskell{a} denotes a name and src_haskell{t} denotes a type expression.
Most Haskell programs usually use those expressions to attach types to top-level definitions.
For instance,
#+BEGIN_SRC haskell-spec
x :: Int
x = 2
foo :: Int -> Int
foo x = a * x
#+END_SRC
\noindent In type expressions simple types are denoted with their names, function types are denoted with arrows, which associate to the right (src_haskell{a -> b -> c == a -> (b -> c)}).
Which, of course, means that a function of $n+1$ arguments can be seen as a function of one argument that returns a function of $n$ arguments.
Which is just currying discussed in the previous section.
Polymorphic functions ("template functions" in C++/Java-speak) are denoted by using src_haskell{forall} operator
#+BEGIN_SRC haskell-spec
id :: forall x . x -> x
id x = x * x
consF :: forall b . b -> (forall a . a -> b) -> b
consF b _ = b
#+END_SRC
\noindent Moreover, "naked" (not under parentheses) leading src_haskell{forall}s can be omitted, thus the above is equivalent to
#+BEGIN_SRC haskell-spec
id :: x -> x
id x = x * x
consF :: b -> (forall a . a -> b) -> b
consF b _ = b
#+END_SRC
\noindent In fact, Haskell 98 does not allow any explicit src_haskell{forall}s, explicit src_haskell{forall}s are a GHC extension named =RankNTypes=.
Finally, while Haskell 98 only allows to attach types to named definitions, GHC with =ScopedTypeVariables= extension allows to attach them to arbitrary expressions.
For instance,
#+BEGIN_SRC haskell-spec
foo :: Int -> Int
foo x = a * (x :: Int)
#+END_SRC
*** Data Types
While pure $\lambda$-calculus can express all computable programs~\cite{barendregt,Barendregt:1991:TPS}, in practice, constructing all values from $\lambda$-terms is very inefficient.
Haskell follows the conventional way to solve this problem by extending $\lambda$-calculus with builtin types, values, and operations that can be efficiently represented and manipulated on conventional hardware, combined with providing ways to combine those types to produce more complex ones.
In Haskell, those builtins include
# FIXME: We use \:: here because else pandoc (incorrectly) parses this as definition lists, this is later fixed in the generated tex with sed in the Makefile
- arbitrarily long integers src_haskell{Integer} like src_haskell{118 \:: Integer} or src_haskell{2 ** 256 \:: Integer} (two to the power 256), there are also types that cover subsets of src_haskell{Integer} like src_haskell{Int}, src_haskell{Word}, src_haskell{Int32}, src_haskell{Word32}, etc;
- rational numbers src_haskell{Rational} like src_haskell{-1.5 \:: Rational} and src_haskell{1/3 \:: Rational} and subsets like src_haskell{Double}, src_haskell{Float}, etc;[fn::
Note how Haskell provides the ideal versions of arbitrary precision out of the box.]
- characters src_haskell{Char} like src_haskell{'A' \:: Char}; and
- strings src_haskell{String} like src_haskell{"Hello, World!" \:: String}.
Haskell also provides two builtin type constructors
- tuples of arbitrary types, like src_haskell{(1, 2, "Hello") \:: (Integer, Rational, String)},
- lists of values of a given type, like src_haskell{[1, 2, 3] \:: [Integer]} and src_haskell{1 : 2 : 3 : [] \:: [Int]} (which are the same thing).
It also provides a way to define tagged unions of Cartesian products of types denoted with src_haskell{data} expressions, for instance
#+BEGIN_SRC haskell-spec
data OptionalIntChar = Null | AnInt Int | AChar Char | Both Int Char
x1 = Null :: OptionalIntChar
x2 = AnInt 1 :: OptionalIntChar
x3 = AChar 'A' :: OptionalIntChar
x4 = Both 1 'A' :: OptionalIntChar
#+END_SRC
\noindent The very first lexeme in each of the blocks between the "src_haskell{|}" symbols is a constructor name (which is a tag to be used for that case in the union), the following ones are types of fields (which are then taken into a Cartesian product).
The names of constructors must be capitalized.
Moreover, data expressions can also take types as arguments, thus making them generic, e.g.
#+BEGIN_SRC haskell-spec
data Maybe a = Nothing | Just a
x1 = Nothing :: Maybe Int
x2 = Just 1 :: Maybe Int
x3 = Just 1 :: Maybe Float
x4 = Just 'A' :: Maybe Char
x5 = Just (\x -> x) :: Maybe (Int -> Int)
#+END_SRC
Functions involving these data types can also be used with pattern matching as if they are builtin types
#+BEGIN_SRC haskell-spec
foo :: Maybe Int -> a -> Int
foo Nothing b = b
foo (Just a) b = a + b
#+END_SRC
Thus, tuples are just a syntax sugar for
#+BEGIN_SRC haskell-spec
data Pair a b = Pair a b
appair f (a, b) = f a b
appair' f (Pair a b) = f a b
data Triple a b c = Triple a b c
-- ...
#+END_SRC
Data type syntax also allows to name to elements of the Cartesian products, for instance
#+BEGIN_SRC haskell-spec
data Quadruple a b c d = Quadruple
{ first :: a
, secound :: b
, third :: c
, fourth :: d
}
#+END_SRC
\noindent which also defines those names into functions extracting corresponding elements from the product
#+BEGIN_SRC haskell-spec
sumQuadruple q = first q + secound q + third q + fourth q
#+END_SRC
Data types can also be recursive, for instance
#+BEGIN_SRC haskell-spec
data List a = Nil -- an empty list
| Cons a (List a) -- prepend @a as the head of @rest
#+END_SRC
In fact, builtin lists can be defined as
#+BEGIN_SRC haskell-spec
data ([]) a = []
| (:) a (List a)
#+END_SRC
\noindent and src_haskell{String} type is actually defined as src_haskell{[Char]} (and string literals are just a special syntax for such data types).
Finally, type expressions can be given names similarly to normal expressions using the src_haskell{type} keyword, and those expressions, too, can include arguments (thus producing "template types" in C++/Java-speak), for instance
#+BEGIN_SRC haskell-spec
type State'' s a = s -> (a, s)
#+END_SRC
\noindent and data types of a single constructor and single field can be defined using src_haskell{newtype} keyword instead of src_haskell{data}, for instance
#+BEGIN_SRC haskell-spec
data State' s a = State' { runState' :: s -> (a, s) }
newtype State s a = State { runState :: s -> (a, s) }
#+END_SRC
The only difference between these definitions is the fact that for src_haskell{newtype} the src_haskell{State} tag is purely syntactic, while src_haskell{State'} of the definition using the src_haskell{data} keyword is going to be stored in memory (which semantically also means that the src_haskell{data} definition introduces lazyness, as one can pattern match on the tag and not on the field, which is impossible with src_haskell{newtype}).
*** Type Classes
The src_haskell{forall} universal quantifier provides a way to implement universally polymorphic functions, that is, functions that use the same terms for different types.
Unfortunately, this universality means that the functions in question can not do much with those arguments of universally quantified types, since those operations must apply to all the possible types.
In fact, they can do nothing except ignoring them and propagating them into subcomputations (that is, copying).
For instance, naively, there cannot be a universal addition operator such that a function
#+BEGIN_SRC haskell-spec
f a b = a + b
#+END_SRC
\noindent could accept arguments of both, say, src_haskell{Int} and src_haskell{Float} types.
Note, however, that in functional programming language nothing prevents us from supplying such a src_haskell{(+)} operator as an argument to the function in question, which would allow us to type it as
#+BEGIN_SRC haskell-spec
f :: (a -> a -> a) -> a -> a -> a
f (+) a b = a + b
#+END_SRC
Then, we can organize sets of such operators and constants into algebraic structures (an object-oriented programming language would call them /interfaces/) and supply functions that need those operators and constants with such structures as arguments, thus getting ad-hoc polymorphism essentially for free
#+BEGIN_SRC haskell-spec
data Monoid a = Monoid
{ zero :: a
, plus :: a -> a -> a
}
intMonoid :: Monoid Int
intMonoid = Monoid intZero intPlus
f :: Monoid a -> a -> a -> a
f (Monoid _ (+)) a b = a + b
#+END_SRC
The only problem with the above is that we have to explicitly construct, apply, and pattern-match arguments of those interface types, which is rather inconvenient.
Which is why Haskell provides "type classes" mechanism which does most of those things automatically.
With type classes one uses src_haskell{class} syntax construct instead of src_haskell{data} to define the type class, src_haskell{instance} syntax construct instead of plain terms to define its instances, separates them with src_haskell{=>} symbol in type signatures, and does not pattern match on those arguments at all.
For instance, the above example would be translated as
#+BEGIN_SRC haskell-spec
class Monoid a where
zero :: a
plus :: a -> a -> a
instance Monoid Int where
zero = intZero
plus = intPlus
f :: Monoid a => a -> a -> a
f a b = a + b
#+END_SRC
Type classes can also extend each other
#+BEGIN_SRC haskell-spec
class Monoid a => Group a where
inverse :: a -> a
instance Group Int where
inverse = intInverse
#+END_SRC
\noindent and instances can be defined as being derived from other instances (thus, effectively, defining functions over type classes)
#+BEGIN_SRC haskell-spec
class Invertible a where
inv :: a -> a
instance (Monoid a, Invertible a) => Group a where
inverse = inv
#+END_SRC
Haskell compiler will then try to apply appropriate instances into all function calls, thus, effectively performing a simple Prolog-like witness search.
Moreover, as with src_haskell{data} keywords GHC Haskell with =MultiParamTypeClasses= extension enabled allows type classes have arbitrary number of arguments.
=FunctionalDependencies= extension also adds a syntax that allows specifying some parameters as dependent on others.
Thus, in fact, one can encode some rather complicated Prolog programs with type classes.
*** Applicatives and Monads
This work primarily concerns itself with src_haskell{Applicative} and src_haskell{Monad} type classes that, ideally (the reality of Haskell's standard library is somewhat less pretty, see \cref{sec:not-tutorial:basic}), make up the following type class hierarchy
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
class Pointed f where
pure :: a -> f a
class Functor f where
fmap :: (a -> b) -> f a -> f b
infixl 4 <*>
class (Pointed f, Functor f) => Applicative f where
(<*>) :: f (a -> b) -> f a -> f b
infixl 1 >>=
class Applicative m => Monad m where
(>>=) :: m a -> (a -> m b) -> m b
#+END_SRC
All of those are discussed in detail in \cref{sec:not-tutorial:basic}.
In this section we shall only try to give the overall description of the latter two structures so that the following sections would make some sense.
The above src_haskell{Applicative} type class, essentially, defines an algebraic structure denoting a generalized function application.
For instance, an identity on Haskell types is obviously an src_haskell{Applicative} with src_haskell{pure = id = \x -> x} and src_haskell{(<*>) = \f x -> f x} being the conventional function application (the one that is usually denoted by simple juxtaposition of terms), but there are many more complex instances of this type class, we shall discuss those in later sections.
The src_haskell{Monad} type class is a bit harder to explain, but essentially, it is a generalization of imperative "semicolon" operator.
To explain why, consider the following pseudo-C program
#+BEGIN_SRC c-spec
x = foo(args);
rest
#+END_SRC
\noindent where src_c{rest} is a subprogram that potentially involves other semicolons.
The above pseudo-code, essentially, just binds the result of evaluation of src_c{foo(args)} to a name src_c{x} in a subprogram named src_c{rest}.
For instance, the following C program would be an instance of the above construction
#+BEGIN_SRC c
something_t main () {
x = foo();
y = bar(x);
return baz(x, y);
}
#+END_SRC
Assuming src_c{foo} is a pure function (without side-effects), the original expression can be encoded in Haskell as
#+BEGIN_SRC haskell-spec
(\x -> rest) (foo args)
#+END_SRC
Thus, the body of the src_c{main} function in the latter program, again, assuming src_c{foo}, src_c{bar}, and src_c{baz} are pure functions, can be encoded in Haskell as
#+BEGIN_SRC haskell-spec
(\x -> (\y -> baz x y) (bar x)) foo
#+END_SRC
\noindent or, equivalently, if we are to denote a flipped application with src_haskell{andThenContinueTo} operator and add some newlines
#+BEGIN_SRC haskell-spec
foo `andThenContinueTo` (\x ->
bar x `andThenContinueTo` (\y ->
baz x y))
#+END_SRC
The src_haskell{(>>=)} operator of the src_haskell{Monad} type class is just one possible way to type such a src_haskell{andThenContinueTo} operator (there are others, which we shall extensively discuss in this work).
Note, however, that the type of src_haskell{(>>=)} actually removes the purity requirements we had to constantly mention above.
In Haskell, impure functions are encoded as pure functions that generate impure "actions" an impure run-time system would eventually /run/ (as opposed to /evaluate/).
In other words, those "actions" are to be interpreted outside of the language, inside the language they are just values (e.g. think system call numbers with attached data or similar).
For instance, assuming src_haskell{newIORef} is such an action that encodes an allocation of a piece of memory on a heap and src_haskell{assign x y} is an action that encodes an assignment of /value/ src_haskell{y} into a piece of memory /pointed by value/ src_haskell{x} (note, however, that src_haskell{assign} then, is a function that takes two arguments and produces such an action), and assuming src_haskell{(>>=)} denotes an opaque function provided by the run-time system that /runs/ an impure action given as its first argument, applies its result to a function given as its second argument, then /runs/ the /result of evaluating/ that as an impure action, the result of which it then returns, then the following impure C program
#+BEGIN_SRC c
void foo(int * x) {
x = 1;
x = 2;
}
void bar() {
int * x = malloc(sizeof(int));
foo(x);
}
#+END_SRC
\noindent can be, more or less, equivalently encoded in Haskell as
#+BEGIN_SRC haskell-spec
foo x =
assign x 1 >>= \_ ->
assign x 2
bar = do
newIORef >>= \x ->
foo x
#+END_SRC
\noindent inlining of which then produces the following expression
#+BEGIN_SRC haskell-spec
newIORef >>= \x ->
assign x 1 >>= _ ->
assign x 2
#+END_SRC
Then, to make this expression evaluate similarly to the C version one needs to invent some values that can be used as encoding for src_haskell{newIORef} and src_haskell{assign x y} and implement an appropriate src_haskell{(>>=)} for them.
That is to say, one needs to make an interpreter that would interpret all references to those symbols adhering to the desired semantics.
That is to say, inside the program one can think of src_haskell{newIORef} and src_haskell{assign} as being elements of a data type run-time system will later interpret.
The point in all of the above is that by generalizing the "semicolon" operator of C into src_haskell{(>>=)} of Haskell one can get many useful benefits.
For instance, note that src_haskell{bar} in the C code above ignores the possible error of src_c{malloc}.
The conventional way to resolve this problem is to either explicitly check for those errors with something like
#+BEGIN_SRC c
void bar() {
int * x = malloc(sizeof(int));
if (x == NULL) abort();
foo(x);
}
#+END_SRC
\noindent or use a library that provides a wrapper around src_c{malloc} that performs such a check and calls src_c{abort} inside.
Safer languages usually only provide the second kind of src_c{malloc} that src_haskell{throw} Out-Of-Memory /exceptions/ or similar.
Which is usually fine for src_haskell{malloc}, since a failure to src_haskell{malloc} usually means that the program can not continue.
But consider, for instance, a less obviously deadly issue of failed logging.
Clearly, a failure to log an event might be a critical problem or non-issue depending on context.
Thus, usually, logging libraries provide several sets of interfaces with different semantics and/or a way to globally configure which of the several logging failure semantics (ignore failures, repeat until success, fail on failure, etc) is desired.
The latter approach, of course, has all the usual problems involving computations using global variables.
The former approach means that computations using an interface with one logging failure semantics can not be reused in computations requiring the other.
By contrast, in Haskell, one could instead have a single logging library with a single zero-configuration interface and several different src_haskell{Monad}s that provide different src_haskell{(>>=)} operators (which either fail, repeat, ignore, etc on logging failures) and switch between those src_haskell{Monad}s depending on context in a way transparent to subcomputations, thus greatly improving in modularity.
In practice, however, defining separate src_haskell{Monad}s for different kinds of computations is so useful that almost every little thing has its own src_haskell{Monad} in Haskell.
The rest of the work will provide numerous examples.
As a final note on the topic we have to mention that this src_haskell{foo >>= \x -> rest} construct is frequent enough that Haskell has a special syntax sugar for it, called src_haskell{do}-syntax, that allows one to write
#+BEGIN_SRC haskell-spec
do
x <- foo
y <- bar x
baz x y
#+END_SRC
\noindent instead of src_haskell{foo >>= \x -> bar x >>= \y -> baz x y}, thus making programs involving src_haskell{do}-syntax look very similar to those written in an imperative languages like C.
** Extended Abstract
@@tex:\label{sec:prelude}@@
If one is to ask a practicing Haskell programmer to succinctly describe src_haskell{Applicative} and src_haskell{Monad} type classes to a practicing programmer in an imperative language, something like "an overloadable function application/call operator" and "an overloadable semicolon operator" would probably be heard.
These structures are useful for a couple of reasons.
- Firstly, using generic operators reduces boilerplate somewhat by allowing for generic combinators (e.g. src_haskell{mapM}).
- Secondly, and more importantly, those structures provide a convenient level of abstraction that hides irrelevant details (of which src_haskell{Either} src_haskell{Monad} that hides the src_haskell{Left} half of the computation until it becomes relevant is a prime example).
Think src_assembly{call} and src_assembly{ret} operators of most conventional assembly languages, a programmer in CPU microcode (or sufficiently RISC assembly) might ask why do you even need those instructions when you can just src_assembly{push}/src_haskell{pop} the instruction pointer and src_assembly{jump}.
Similarly, a programmer for IBM 650 might argue that even linear sequencing of instructions and the instruction pointer are superfluous, each instruction could just explicitly specify the address of the next instruction.
Similarly, for src_haskell{Applicative} and src_haskell{Monad}, while one could just use particular src_haskell{(<*>)} and src_haskell{(>>=)} implementations explicitly, having those operators to represent an even higher level of abstraction can be even more convenient.
(Though, it can be problematic to show that convenience to a programmer in a language lacking the means to express it, like with src_haskell{Either} src_haskell{Monad}.)
Interestingly however, after explaining why src_haskell{Applicative} and src_haskell{Monad} are useful and pointing that they are indeed very popular in Haskell programs one will be faced with the fact that, apparently, there are not many commonly applicable instances of these structures.
In fact, just src_haskell{Either} and src_haskell{State} together seem to cover almost everything:
- computations that might fail usually wrap themselves into src_haskell{Either} (\cref{sec:either}),
- a src_haskell{main} function in a Haskell program, more or less, simply interprets a src_haskell{State} transformer (\cref{sec:state}) over a src_haskell{RealdWorld} that computes program outputs from program inputs (i.e. src_haskell{IO} src_haskell{Monad} of \cref{sec:io}, though it can have other interpretations, see \cref{rem:io-caveats}),
- most other things are either particular cases (e.g. src_haskell{Maybe}), compositions of those two (parsing, for instance, is just a composition of src_haskell{State} and src_haskell{Either} with src_haskell{Stream}s in place of the src_haskell{RealdWorld}, see \cref{sec:parser-combinators}), or mechanical transformations (e.g. Scott-encoding, see \cref{sec:scott-encoding}) of them.
The fact that src_haskell{Either} and src_haskell{State} src_haskell{Applicative}s and src_haskell{Monad}s can express so much makes it even more interesting to carefully look at the frequently used things they, apparently, /can not/ express.
Firstly, note that apart from the pure src_haskell{Either} and its particular cases Haskell provides a bunch of other mechanisms for error handling: most notably, imprecise exceptions (see \cref{sec:imprecise}) and several different type classes claiming to implement generic src_haskell{throw} and src_haskell{catch} with slightly different semantics (see \cref{sec:monadic-generalizations}).
Secondly, note that src_haskell{type State s a = s -> (a, s)} uses a single type src_haskell{s} on both sides of the arrow.
If one is to take a fundamentalist view that all computations are just compositions of state transformers and should be expressed as such, then it is immediately apparent that src_haskell{State} is too restrictive for the general use case as it can not express state transitions between arbitrary data types.
In other words, while a fundamentalist Haskell programmer could feel content parsing src_haskell{Stream}s (in particular, src_haskell{String}s) into data types with the help of a parser combinator library like Parsec~\cite{Hackage:parsec3111}, to do most other things he/she would have to succumb to using several different approaches to error handling while pattern-matching data types manually or with libraries such as SYB~\cite{Laemmel:2003:SYB}, Uniplate~\cite{Mitchell:2007:Uniplate}, Multiplate~\cite{Hackage:multiplate003}, and Lenses~\cite{Kmett:Lens, Hackage:lens417}.
Which is not to say that doing all those things is inherently bad, but it is interesting to see just how much can be done with just src_haskell{Either}, src_haskell{State}, src_haskell{Applicative}, and src_haskell{Monad} and their natural extensions, that is to say that it is interesting to see how much can be done with very basic theoretical constructs and their combinations.
The purpose of this work is to show that the set of things expressible using these structures is surprisingly large.
Or, more specifically, to show that /all/ of the problems commonly thought of as requiring special care mentioned above can in fact be solved by reusing those well-known structures with minor (if any) modifications.
*** Headline Contributions
@@tex:\label{sec:contributions}@@
Specifically, every item in the following list, to our best knowledge, is a headline contribution.
- 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{pure} (src_haskell{return}) and src_haskell{(>>=)} (src_haskell{bind}) operators
#+BEGIN_SRC haskell-spec
pure :: 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
pure :: 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{pure} 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{pure} 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 \cref{sec:instances:more}, 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:products}.
- 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{Monad}ic src_haskell{sequence} combinator (see \cref{sec:instances:parser-combinators}).
- 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.
- We notice that many practically interesting structures can be described as Cartesian product of a structure handling errors and a structure handling computations (\cref{sec:products}), which suggests an interesting direction is programming language design (see \hyperref[sec:conclusions]{conclusions}).
- We notice that many src_haskell{Applicative} computations can be interpreted as providing a /mechanism/ to construct a data type with "ports" "pluggable" by subcomputations (\cref{sec:ale:motivation,sec:definition}).
We observe that it is this property that makes them so much more convenient in practice than the usual way of building the same computations using conventional composition.
- We distill this observation into a more general algebraic structure of (and/or technique for expressing) "src_haskell{Applicative}-like" computations and demonstrate several other (that is, non-src_haskell{Applicative}) instances of this structure (\cref{sec:deriving-the-technique,sec:implementation}),
which includes a curious family of structures that work with Scott-encoded data types as if they are heterogeneous lists of typed values (\cref{sec:scott}).
- Then, we show that there is, in fact, an infinite family of such "src_haskell{Applicative}-like" structures (\cref{sec:general-case}).
This family can be succinctly described as a family of computations for generalized multi-stack machines with arbitrary data types and/or functions as "stacks" (\cref{sec:implementation,sec:formally}).
- Then, we observe that our "src_haskell{Applicative}-like" is actually a natural generalization of the conventional src_haskell{Applicative} into dependent types (\cref{sec:ale:deptypes}).
- We notice that src_haskell{Monad}ic parser combinators can be generalized into indexed src_haskell{Monad}s thus allowing one to "parse" (transform between) arbitrary data types/trees (\cref{sec:pim}).
** Introduction to the Basic Structures of Haskell
@@tex:\label{sec:not-tutorial:basic}@@
While algebraic structures used in this work are simple, there are a lot of them.
This chapter is intended as a reference point for all algebraic structures relevant in the context of this document (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 a tutorial introduction to the structures in question: when discussing a structure we shall only show the most primitive examples of its usage, if any at all.
To get a deeper understanding of those structures and their use the reader will have to look into the examples given in the original papers and sources (which we shall cite) and, most likely, do some programming practice.
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 a common src_haskell{Pointed} type class (see \cref{sec:applicative-functor}) instead of conventional duplication of 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, the author feels like most remarks and footnotes are not).
On the first reading we advise to skip straight to \cref{sec:not-tutorial:non-basic} and refer back to this section on demand.
#+BEGIN_SRC haskell :tangle TngPrelude.hs :exports none
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE 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?
module TngPrelude
( module TngPrelude
, module Prelude
, module Data.Typeable
, module Data.List
) where
-- 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 TngSyntaxCheckOnly.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 section describes the simplest type classes used in this work.
**** 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 work we shall use the original definition as is.]
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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}.
Arguably, src_haskell{Monoid}s provide the simplest (after "just abort the program") "error handling" mechanism: 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 TngPrelude.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 structures that follow are src_haskell{Applicative} src_haskell{Functor}s~\cite{mcbride-paterson-08}.
src_haskell{GHC.Base} from =base=~\cite{Hackage:base4900} package defines those two algebraic structures as follows
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.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 work (we will never use them explicitly).
Meanwhile, for the purposes of this work 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 TngPrelude.hs :exports none
-- copy-paste
class Functor f where
fmap :: (a -> b) -> f a -> f b
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 p = fmap (:) p <*> many p
many :: f a -> f [a]
many p = some p <|> 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 p == fmap (:) p <*> many v
many p == some p <|> 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 TngPrelude.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 section describes algebraic structures that involve src_haskell{Monad} type class and its instances.
**** src_haskell{Monad}
@@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 TngSyntaxCheckOnly.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, the author feels 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 TngPrelude.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
If one is to swap the order of arguments of src_haskell{(>>=)} then the result is very similar to the type of src_haskell{($)} (which is just a low-infix-priority version of the normal function application operator) and src_haskell{(<*>)} operators.
Essentially, src_haskell{(>>=)} is src_haskell{(<*>)} that allows to introduce lambdas "outside of context" of src_haskell{m} but nevertheless keeps results confined to src_haskell{m}.
Compare the following, also see \cref{rem:monad-as-app}.
#+BEGIN_SRC haskell-spec
($) :: (a -> b) -> a -> b
(<*>) :: m (a -> b) -> m a -> m b
bind :: (a -> m b) -> m a -> m b
#+END_SRC
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 TngPrelude.hs
(>>) :: Monad m => m a -> m b -> m b
a >> b = a >>= const b
-- a >>= \_ -> b
#+END_SRC
The following sections 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 TngPrelude.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 the author could not find a reference with a simple proof of that fact, hence this section shall give one.
#+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 TngPrelude.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 TngPrelude.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
#+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{(>=>)} and, thus, src_haskell{(>>=)} combine function composition/application (the whole type) with lambda introduction "outside of context".
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
**** src_haskell{Monad}'s src_haskell{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 TngSyntaxCheckOnly.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 TngPrelude.hs
class Monad m => MonadFail m where
fail :: String -> m a
fail s = error s
#+END_SRC
As of writing of this work 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} src_haskell{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 TngPrelude.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} src_haskell{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 TngPrelude.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 TngPrelude.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 TngPrelude.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} src_haskell{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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 document version where appropriate (it can still be observed in the Literate Haskell version).
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 sections 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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 work 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 TngPrelude.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 TngPrelude.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}
#+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}
@@tex:\label{sec:reader}@@
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 TngPrelude.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 TngPrelude.hs :exports none
instance Monad m => Functor (ReaderT s m) where
fmap = liftM
instance Monad m => Applicative (ReaderT s m) where
(<*>) = ap
#+END_SRC
Essentially, src_haskell{type Reader s a = s -> a}, thus src_haskell{Reader r} is just a "function from src_haskell{r}".
Its src_haskell{Pointed} instance simply wraps a given value into a constant function while src_haskell{(>>=)}, essentially, does src_haskell{Identity} computations while chaining src_haskell{r} around.
In other words, src_haskell{Reader} src_haskell{Monad} represents computations in immutable global context (e.g. think environment variables provided by the OS).
**** src_haskell{State}
@@tex:\label{sec:state}@@
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 work, so we shall ignore it) from =transformers=~\cite{Hackage:transformers0520} package equivalently to
#+BEGIN_SRC haskell :tangle TngPrelude.hs
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
type State s = StateT s Identity
-- or, beta-equivalently
-- newtype State s a = State { runState :: s -> (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 TngPrelude.hs :exports none
instance Monad m => Functor (StateT s m) where
fmap = liftM
instance Monad m => Applicative (StateT s m) where
(<*>) = ap
#+END_SRC
Essentially, src_haskell{type State s a = s -> (a, s)}.
As we seen above, src_haskell{ReaderT} simply applies variable src_haskell{s} throughout its whole computation via its src_haskell{(>>=)} operator thus supplying computations with a global immutable context, that is, immutable state.
Meanwhile, src_haskell{StateT} chains its src_haskell{s} between computations, thus providing computations with a mutable state.
#+BEGIN_SRC haskell :tangle TngPrelude.hs
get :: State s s
get = StateT $ \s -> pure (s, s)
put :: s -> State s ()
put s = StateT $ \_ -> pure ((), s)
#+END_SRC
*** Imprecise Exceptions
@@tex:\label{sec:imprecise}@@
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 sections 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:state}) on src_haskell{State# RealWorld} (definitions of both of which are beyond the scope of this work)
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 work, 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 work 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 TngSyntaxCheckOnly.hs
raise# :: a -> b
raise# = raise#
catch# :: IO# a -> (b -> IO# a)
-> IO# a
catch# = catch#
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.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 work.
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 TngSyntaxCheckOnly.hs
class Typeable a where
-- magic beyond the scope of this work
#+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 TngSyntaxCheckOnly.hs
cast :: forall a b
. (Typeable a, Typeable b)
=> a -> Maybe b
#+END_SRC
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs :exports none
-- Beyond the scope of this work
cast = cast
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 TngPrelude.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 (actually src_haskell{raiseIO#}s, since its a precise exception, this will be discussed in \cref{sec:intro:raiseio-throwio}) again on failure.
#+BEGIN_SRC haskell :tangle TngPrelude.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"; this fact can be ignored for the purposes of this work) which is yet another special GHC runtime function (this time, extentionally equal to its definition, i.e. identity).
#+BEGIN_SRC haskell :tangle TngPrelude.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 work 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 TngPrelude.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 TngPrelude.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 work.
Interested readers are referred to the source code of src_haskell{GHC.Err}.
*** Precise src_haskell{raiseIO#} and src_haskell{throwIO}
@@tex:\label{sec:intro:raiseio-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 TngSyntaxCheckOnly.hs
raiseIO# :: a -> IO# b
raiseIO# = raiseIO#
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.hs :exports none
{-# NOINLINE raiseIO# #-}
raiseIO# :: a -> IO# b
raiseIO# a b = (GP.raiseIO#) a b
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.hs
data SomethingElse = SomethingElse
instance Exception SomethingElse where
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.hs :exports none
instance Show SomethingElse where
show _ = "something"
deriving instance Typeable SomethingElse
#+END_SRC
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 TngIntroPatterns.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 }
-- These are GHC < 8.6 only, GHC 8.6 uses MonadFail
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 sections we have seen a plethora of slightly different error handling structures with different src_haskell{throw} and src_haskell{catch} operators.
In this section 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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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 TngPrelude.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.
** Introduction to Some Non-basic Structures of Haskell
@@tex:\label{sec:not-tutorial:non-basic}@@
This section, logically, is a continuation of \cref{sec:not-tutorial:basic}.
However, in contrast to that section this section discusses non-basic structures that are of particular importance to the rest of the work.
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 section.
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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)
#+BEGIN_SRC haskell :tangle TngPrelude.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 machine instruction level 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
$$\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 TngPrelude.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 TngPrelude.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 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 section 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 TngPrelude.hs
newtype Cont r a = Cont
{ runCont :: (a -> r) -> r }
#+END_SRC
\noindent with the following src_haskell{Monad} instance
#+BEGIN_SRC haskell :tangle TngPrelude.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 TngPrelude.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 TngSyntaxCheckOnly.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 TngPrelude.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 TngPrelude.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 TngPrelude.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}@@
Parser combinators, as their name suggests, are combinators (closed terms) that are designed with the purpose of building parsers (functions from src_haskell{Stream}s to trees/structured data) by combining simpler parsers into progressively more and more complex ones.
The resulting parsers usually have worse performance than those produced by parser generators (e.g. Yacc~\cite{Yacc} and Bison~\cite{Bison}), but parsers expressed using parsers combinators can be much simpler to understand as they are commonly built using high-level declarative descriptions (since such parsers are first-class objects of the language, all the usual compositional powers of the target language apply), unlike for the usual way of describing grammars with EBNF and similar and then generating an opaque parser for the target language in a single step.
In the context of error handling, while parser combinators are not by themselves a general error handling mechanism, in practice, parsers frequently need to handle failed parsing attempts using rather complex strategies, thus parser combinator libraries usually provide rather elaborate error handling mechanisms.
src_haskell{Monad}ic parser combinators, as their name suggests, are parser combinators that also form a src_haskell{Monad}.
The most popular src_haskell{Monad}ic parser combinator libraries for Haskell are Parsec~\cite{Hackage:parsec3111, Leijen:2001:PDS}, Attoparsec~\cite{Hackage:attoparsec01310}, and Megaparsec~\cite{Hackage:megaparsec630}.
In general, such structures can possess a wide variety of semantics and implementations, to mention just a few possible dimensions of the space:
- they can parse various classes of parsing grammars (PEG~\cite{Ford:2004:PEG}, $LL\infty$, etc; admitting left recursion, or not),
- 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 simple src_haskell{String}s, lists of arbitrary elements, or impure src_haskell{Stream}s (in general, a src_haskell{Stream} is any structure that can produce elements of input on demand, e.g.
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
class Stream s m a where
getNextElement :: s -> m (Maybe (a, s))
-- where Nothing signifies end-of-stream / end-of-file
#+END_SRC
or similar; of course, lists and thus src_haskell{String}s, which are lists of src_haskell{Char}s, also can be trivially represented this way),
- track position in the input src_haskell{Stream},
- allow for 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 work.
Internal structures used to implement parsing combinators presented throughout this document will be very similar to those used in Parsec and Megaparsec.
They, too, parse PEG languages and are built by combining the src_haskell{State} src_haskell{Monad} over input src_haskell{Stream} with a structure for handling failed parsing attempts.
Meanwhile, Attoparsec is built using a somewhat different internal structure (though, it can be argued that it, too, is a variant of src_haskell{State}) which we shall not discuss in this work (thus reading its sources is highly recommended for educational reasons).
All aforementioned libraries also Scott-encode their internals for efficiency, we shall skip that step for clarity reasons, except for \cref{sec:instances:eio} where we shall demonstrate Scott-encoding applied to, essentially, the same algebraic structure.
From the rest of the possible dimensions listed above in this document we shall only discuss "backtrack vs. not" and "programmer-provided error types".
Detailed implementations of other features can be studied by following respective references.
**** Simple src_haskell{Monad}ic 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:state}) 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 TngPrelude.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 TngPrelude.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 TngPrelude.hs :exports none
instance Functor (SParser s e) where
fmap = liftM
instance Applicative (SParser s e) where
(<*>) = ap
#+END_SRC
#+BEGIN_theorem
src_haskell{SParser} satisfies src_haskell{Monad} laws.
#+END_theorem
#+BEGIN_proof
It is a composition of src_haskell{StateT} and src_haskell{ExceptT} src_haskell{MonadTrans}formers.
#+END_proof
In fact, the above definition is (almost) exactly the definition used in Ponder~\cite{Hackage:ponder001} parser combinator library (it exports the general src_haskell{m} instead of substituting it with src_haskell{Identity}).
We just need to define an src_haskell{Alternative} instance for handing failed parsing attempts
#+BEGIN_SRC haskell :tangle TngPrelude.hs
instance Monoid e => Alternative (SParser s e) where
empty = SParser $ \s -> Left mempty
f <|> g = SParser $ \s -> case runSParser f s of
Right x -> Right x
Left e -> case runSParser g s of
Right x -> Right x
Left e' -> Left (e `mappend` e')
#+END_SRC
\noindent and it already gives us enough headroom to define some primitive parsers and a couple of examples
#+BEGIN_SRC haskell :tangle TngPrelude.hs
type Parser = SParser String [String]
eof :: Parser ()
eof = SParser $ \s -> case s of
[] -> Right ((), s)
_ -> Left ["expected eof"]
char :: Char -> Parser ()
char x = SParser $ \s -> case s of
[] -> Left ["unexpected eof"]
(c:cs) -> if (c == x)
then Right ((), cs)
else Left ["expected `" ++ [x] ++ "' got `" ++ [c] ++ "'"]
string :: String -> Parser ()
string [] = pure ()
string (c:cs) = char c >> string cs
testSParser = runSParser (string "foo") "foo bar"
== Right((), " bar")
&& runSParser (string "abb" <|> string "abc") "aba"
== Left ["expected `b' got `a'", "expected `c' got `a'"]
#+END_SRC
**** \dots with Full Access to the State
@@tex:\label{sec:parser-combinators:with-access}@@
While the definitions above are very simple and get the parsing job done, src_haskell{SParser} provides no way to access the state of the parser on error, which can make it somewhat inconvenient.
However, a simple modification of the type that moves src_haskell{Either} into the tuple
#+BEGIN_SRC haskell-spec
newtype EParser s e a = EParser
{ runEParser :: s -> (Either e a, s) }
#+END_SRC
\noindent which, of course, in isomorphic to
#+BEGIN_SRC haskell :tangle TngPrelude.hs
newtype EParser s e a = EParser
{ runEParser :: 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 and definitions of the primitive combinators essentially identical to those described in the previous section.
#+BEGIN_SRC haskell :tangle TngPrelude.hs :exports none
-- yep, copy-paste
instance Pointed (EParser s e) where
pure a = EParser $ \s -> Right (a, s)
instance Monad (EParser s e) where
p >>= f = EParser $ \s ->
case runEParser p s of
Left x -> Left x
Right (a, s') -> runEParser (f a) s'
instance Functor (EParser s e) where
fmap = liftM
instance Applicative (EParser s e) where
(<*>) = ap
#+END_SRC
#+BEGIN_theorem
src_haskell{EParser} satisfies src_haskell{Monad} laws.
#+END_theorem
#+BEGIN_proof
By case analysis.
Also see the proof of~\cref{thm:with-heuristic}.
#+END_proof
src_haskell{MonadTrans}former version of src_haskell{EParser} can be trivially obtained by adding src_haskell{Monad}ic index src_haskell{m} after the arrow (i.e. by exposing the internal src_haskell{Monad} of the original src_haskell{MonadTrans} stack) and correspondingly tweaking all primitive combinators and type signatures.
**** Rollback vs. Not, Programmer-provided Error Types
@@tex:\label{sec:parser-combinators:variants}@@
Note that since src_haskell{Left} results of the src_haskell{runSParser} produce no state, the above definition of src_haskell{(<|>)} operator has no choice but to supply the same state to both alternatives.
In other words, src_haskell{(<|>)} of src_haskell{SParser}, from the point of view of its second argument, always rolls-back the state on failure.
Meanwhile, there are six variants of that term for src_haskell{EParser}
#+BEGIN_SRC haskell-spec
f `altEPVariant` g = EParser $ \s -> case runEParser f s of
Right x -> Right x
Left (e, s') -> case runEParser g X of
Right x -> Right x
Left (f, s'') -> Left (f, Y)
#+END_SRC
\noindent with src_haskell{X} being one of src_haskell{s, s'} and src_haskell{Y} being one of src_haskell{s, s', s''}.
Let us particularly note the following two of those six
#+BEGIN_SRC haskell :tangle TngPrelude.hs
f `altEPR` g = EParser $ \s -> case runEParser f s of
Right x -> Right x
Left (e, _) -> case runEParser g s of
Right x -> Right x
Left (e', _) -> Left (e `mappend` e', s)
f `altEPC` g = EParser $ \s -> case runEParser f s of
Right x -> Right x
Left (e, s') -> case runEParser g s' of
Right x -> Right x
Left (e', s'') -> Left (e `mappend` e', s'')
#+END_SRC
The src_haskell{altEPR} is a direct analogue of the src_haskell{(<|>)} operator of src_haskell{SParser}, it runs both alternatives over the same state and returns that same state as the result on failure.
Conversely, src_haskell{altEPC} tries to run the next alternative using the state produced by the previous one, and returns the rightmost state as the result on failure.
#+BEGIN_theorem
@@tex:\label{thm:with-heuristic}@@
Both src_haskell{altEPR} and src_haskell{altEPC} are associative, but the other four variants of src_haskell{altEPVariant} are not.
#+END_theorem
#+BEGIN_proof
By case analysis.
Note that to convince yourself of the fact that src_haskell{altEPR} and src_haskell{altEPC} are associative it is enough to observe that in src_haskell{a <|> b <|> c} for these two operators
- src_haskell{Right} is a zero,
- in the absence of zeros, the resulting value of src_haskell{e} is always the same src_haskell{mconcat} of all the intermediate values of src_haskell{e},
- the value of src_haskell{s}
- always stays the same in src_haskell{altEPR},
- always propagates one src_haskell{runEParser}-step to the right in src_haskell{altEPC}.
Which means that parentheses can't influence anything for either function.
The same observation that the state either always stays the same or propagates one step at a time can be used to prove associativity of other similar operators for structures derived from src_haskell{State} src_haskell{Monad}.
#+END_proof
Thus, src_haskell{Alternative} instance for src_haskell{EParser} can use either of the two operators and still satisfy the laws of src_haskell{Alternative}.
#+BEGIN_SRC haskell :tangle TngPrelude.hs
instance Monoid e => Alternative (EParser s e) where
empty = EParser $ \s -> Left (mempty, s)
(<|>) = altEPR
-- or, alternatively
-- (<|>) = altEPC
#+END_SRC
#+BEGIN_theorem
The src_haskell{Alternative} instance for src_haskell{SParser} from~\cref{sec:parser-combinators:without-access} and both of the above instances for src_haskell{EParser} satisfy src_haskell{Alternative} laws.
#+END_theorem
#+BEGIN_proof
By the argument of \cref{thm:with-heuristic}.
#+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 :: EParser s e a -> EParser s e a
#+END_SRC
Thus, given a parser for the rolling-back src_haskell{(<|>)} one can produce an equivalent parser for non-rolling-back src_haskell{(<|>)} by wrapping all the first arguments of all calls to src_haskell{(<|>)} with src_haskell{try}s.
This may sound like a pointless complication but it has some performance advantages since some of that wrapping can be skipped when src_haskell{a <|> b} start by parsing the same prefix, which allows one to write parsers that can parse arbitrary long inputs in constant memory~\cite{Leijen:2001:PDS}.[fn::@@tex:\label{fn:no-rollback}@@
Though, the author feels that introducing operators that explicitly drops pieces of the old state is a better approach since it is hard to reason about parsers using non-rolling-back src_haskell{(<|>)} without knowing their internals ("How much can it consume before failing, again?").
But that discussion is out of scope of this work.
]
Semantics-wise our src_haskell{EParser} 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 src_haskell{Stream} and a bunch of primitive parsers, which we leave as an exercise to the interested reader.
Interestingly, this exact explicit 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.
Parsec and Attoparsec use fixed error types that form src_haskell{Monoid}s instead.
Ponder gets pretty much the same src_haskell{Alternative} instance as the one used by src_haskell{SParser} above for free by being constructed from standardized src_haskell{MonadTrans}former parts.
*** Indexed src_haskell{Monad}s
@@tex:\label{sec:not-tutorial:indexed-monads}@@
src_haskell{Control.Monad.Indexed} module of =indexed=~\cite{Hackage:indexed013} defines an indexed variant of the src_haskell{Pointed}, src_haskell{Functor}, src_haskell{Applicative}, src_haskell{Monad} type class hierarchy.
In this work we shall use the following equivalent set of definitions.
#+BEGIN_SRC haskell :tangle TngPrelude.hs
class IxPointed m where
ipure :: a -> m i i a
class IxFunctor f where
ifmap :: (a -> b) -> f i j a -> f i j b
infixl 4 <*+>
class (IxPointed m, IxFunctor m) => IxApplicative m where
(<*+>) :: m i j (a -> b) -> m j k a -> m i k b
infixl 1 >>=+
class IxApplicative m => IxMonad m where
(>>=+) :: m i j a -> (a -> m j k b) -> m i k b
-- (>>) equivalent for (>>=+)
(>>+) :: IxMonad m => m i j a -> m j k b -> m i k b
a >>+ b = a >>=+ const b
-- IxApplicative from IxMonad
iap :: IxMonad m => m i j (a -> b) -> m j k a -> m i k b
iap a b = a >>=+ \f -> b >>=+ \a -> ipure (f a)
-- IxFunctor from IxApplicative
iliftM :: IxApplicative m => (a -> b) -> m i j a -> m i j b
iliftM f a = (ipure f) <*+> a
#+END_SRC
**** Indexed src_haskell{State} src_haskell{Monad}
@@tex:\label{sec:not-tutorial:indexed-state}@@
src_haskell{IxMonad} is not a particularly popular algebraic structure, but it well-known enough to have its own Hackage library.
Its usefulness in the context of this work comes from the fact that if one is to generalize the src_haskell{State} type
#+BEGIN_SRC haskell-spec
newtype State s a = State { runState :: s -> (a, s) }
#+END_SRC
\noindent a little producing the following type we shall call src_haskell{IxState}
#+BEGIN_SRC haskell :tangle TngPrelude.hs
newtype IxState i j a = IxState { runIxState :: i -> (a, j) }
#+END_SRC
\noindent then the terms of operators of src_haskell{Monad State} can also be used as terms for src_haskell{IxMonad IxState} without modifications
#+BEGIN_SRC haskell :tangle TngPrelude.hs
instance IxPointed IxState where
ipure a = IxState $ \i -> (a, i)
instance IxMonad IxState where
m >>=+ f = IxState $ \i ->
let (a, j) = runIxState m i
in runIxState (f a) j
instance IxFunctor IxState where
ifmap = iliftM
instance IxApplicative IxState where
(<*+>) = iap
#+END_SRC
*** Other Variants of src_haskell{MonadCatch}
@@tex:\label{sec:other-monadic-generalizations}@@
Finally, returning back to the topic src_haskell{throw} and src_haskell{catch}, 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}.
* Exceptionally src_haskell{Monad}ic Error Handling
@@tex:\label{sec:eme}@@
** Motivation
#+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 work 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 work 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 work): 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 work we shall demonstrate a fairly straightforward but surprisingly useful solution to this problem.
\Cref{sec:init,sec:type-of-catch} derive a solution for the problem in question by purely pragmatic reasoning and then prove that the resulting structure is the only possible solution matching conventional operational semantics for src_haskell{throw} and src_haskell{catch} operators.
\Cref{sec:conjoinedly-monadic} gives a proper formal definition for the resulting structure.
\Cref{sec:instances:either} discusses the most trivial instance of the structure: the src_haskell{Either} type.
\Cref{sec:encodings} discusses the issue of encoding of the resulting formal structure in Haskell and similar languages.
\Cref{sec:instances:more} discusses many more instances of the structure.
\Cref{sec:products} shows that the resulting structure can be generalized even further by decomposing it into a Cartesian product with interaction laws and replacing parts with more general structures.
\Cref{sec:eme:discussion} discusses the consequences of these observations and the general picture.
** Derivation
@@tex:\label{}@@
*** The Nature of an Error
@@tex:\label{sec:init}@@
#+BEGIN_SRC haskell :tangle TngEmeDerivation.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 TngEmeDerivation.hs
data C e a
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeDerivation.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 TngEmeDerivation.hs
pure :: a -> C e a
(>>=) :: C e a -> (a -> C e b) -> C e b
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeDerivation.hs :exports none
pure = 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 TngEmeDerivation.hs
throw :: e -> C e a
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeDerivation.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{pure}, src_haskell{(>>=)}, src_haskell{throw}, and src_haskell{catch} operators satisfying
1. @@tex:\label{dfn:structure:monad}@@
src_haskell{pure} 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:pure-catch}@@
src_haskell{pure a `catch` f == pure a} ("src_haskell{pure} 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
pure a `catch` f
#+END_SRC
The expected semantics of src_haskell{catch} requires (by \cref{dfn:structure:pure-catch} of \cref{dfn:structure})
#+BEGIN_SRC haskell-spec
pure a `catch` f == pure a
#+END_SRC
Note that the most general type for src_haskell{pure 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{pure} 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{pure} 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:pure-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` (\_ -> pure a) == pure 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 TngEmeDerivation.hs
catch :: forall a e f . C e a -> (e -> C f a) -> C f a
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeDerivation.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{pure}, 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
pure a `catch` f == pure a
throw e `catch` (\_ -> pure a) == pure a
throw e `catch` (\_ -> throw f) == throw f
#+END_SRC
#+END_proof
*** Formal Account: 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{pure} 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}),
\noindent and assuming
- the names of src_haskell{Monad} operators in the second index of src_haskell{m} are src_haskell{pure} and src_haskell{(>>=)},
- the names of src_haskell{Monad} operators in the first index are src_haskell{throw} and src_haskell{catch},
\noindent the following equations hold
1. @@tex:\label{dfn:proper:pure-catch}@@
src_haskell{pure x `catch` f == pure 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.
#+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,
\noindent and assuming
- the names of src_haskell{MonadFish} operators in the second index are src_haskell{pure} and src_haskell{(>=>)},
- the names of src_haskell{MonadFish} operators in the first index are src_haskell{throw} and src_haskell{handle},
\noindent the following equations hold
1. @@tex:\label{dfn:fishy:pure-catch}@@
src_haskell{pure `handle` f == pure},
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{pure} is a left zero for src_haskell{catch} (src_haskell{handle}) and src_haskell{throw} is a left zero for src_haskell{(>>=)}
(src_haskell{(>=>)}).
*** Instance: 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 TngEmeMain.hs :exports none
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE StandaloneDeriving, MagicHash, UnboxedTuples, RebindableSyntax #-}
{-# LANGUAGE RankNTypes, ScopedTypeVariables, ExistentialQuantification #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, UndecidableInstances #-}
import TngPrelude
import GHC.Prim (State#, RealWorld)
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.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{pure} 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{pure x `catchE` f == pure 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}.
Thus, using, the encoding of~\cref{sec:encodings}, we can write:
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
instance ConjoinedMonads Either where
cpure = pure
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.
In fact, in~\cite{Gonzalez:2012:SEH} Gabriel Gonzalez, the author of the =errors=~\cite{Hackage:errors230} 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, without proofs or claims of general applicability).
He then mentions that the fact itself was first pointed out to him by Elliott Hird who named the other src_haskell{Monad} the "success src_haskell{Monad}".
From this point of view, the contribution of \cref{sec:init,sec:type-of-catch,sec:conjoinedly-monadic} is that they generalize this observation into \cref{dfn:proper}, prove \cref{thm:catch-type}, and notice the general duality discussed in footnote~\ref{fn:its-dual}.
Then, the main point of this whole part of the work 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.
*** Formal Account: Haskell Encoding
@@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 TngSyntaxCheckOnly.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 -> pure (Right r)
#+END_SRC
- no src_haskell{Monad}ic parser 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} 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
pure :: 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
\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
#+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 (\a -> m e a)) -- `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 part of the work 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 (note that this is an src_haskell{instance}, not a src_haskell{class}) which, arguably, can be considered good enough, though, again, not very convenient in practice.
The purposes of this work, 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 following variation on very first definition of src_haskell{ConjoinedMonads} from above for simplicity.
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
-- We have to add the `c` prefix here so that it won't conflict with other definitions.
class ConjoinedMonads m where
cpure :: 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
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).
** Non-trivial Instances
@@tex:\label{sec:instances:more}@@
*** 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
cpure :: a -> m a
cbind :: 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 TngEmeMain.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
handleOrThrowAgain 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 . handleOrThrowAgain
#+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.
The author feels 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{handleOrThrowAgain}.
#+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{handleOrThrowAgain} 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
*** 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}.
**** The Boring Part
@@tex:\label{sec:instances:parser-combinators:inevitable}@@
To start off, let us continue using the definitions of src_haskell{SParser} and src_haskell{EParser} types from \cref{sec:parser-combinators}.
Similarly to src_haskell{Alternative} (\cref{sec:alternative}) instances of~\cref{sec:parser-combinators:variants}, the src_haskell{Monad} instances in index src_haskell{e} for those types can be discovered by going through all free functions of appropriate types satisfying src_haskell{Monad}ic laws.
Thus, similarly, there is a single possible implementation for both src_haskell{pure}s in index src_haskell{e},
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
throwSP :: e -> SParser s e a
throwSP e = SParser $ \_ -> Left e
throwEP :: e -> EParser s e a
throwEP e = EParser $ \s -> Left (e, s)
#+END_SRC
\noindent one possible implementation for src_haskell{(>>=)} of src_haskell{SParser}, and two possible implementations for src_haskell{(>>=)} of src_haskell{EParser},
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
catchSP :: SParser s e a -> (e -> SParser s f a) -> SParser s f a
catchSP p f = SParser $ \s ->
case runSParser p s of
Right x -> Right x
Left e -> runSParser (f e) s
catchEPR :: EParser s e a -> (e -> EParser s f a) -> EParser s f a
catchEPR p f = EParser $ \s ->
case runEParser p s of
Right x -> Right x
Left (e, _) -> runEParser (f e) s
catchEPC :: EParser s e a -> (e -> EParser s f a) -> EParser s f a
catchEPC p f = EParser $ \s ->
case runEParser p s of
Right x -> Right x
Left (e, s') -> runEParser (f e) s'
#+END_SRC
\noindent all of which satisfy src_haskell{Monad}ic laws.
Similarly to~\cref{sec:parser-combinators:variants}, src_haskell{catchEPR} does backtracking on failures and src_haskell{catchEPC} proceeds with the current state.
#+BEGIN_theorem
@@tex:\label{thm:instances:parser-combinators}@@
src_haskell{SParser} is an instance src_haskell{ConjoinedMonads}.
src_haskell{EParser} is an instance of src_haskell{ConjoinedMonads} for both versions of src_haskell{catchEP}.
#+END_theorem
#+BEGIN_proof
src_haskell{Monad} laws for src_haskell{catchSP} and src_haskell{catchEP} follow from the corresponding laws for src_haskell{(>>=)} of \cref{sec:parser-combinators}.
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 TngEmeMain.hs
instance ConjoinedMonads (SParser s) where
cpure = pure
cbind = (>>=)
cthrow = throwSP
ccatch = catchSP
instance ConjoinedMonads (EParser s) where
cpure = pure
cbind = (>>=)
cthrow = throwEP
ccatch = catchEPR
-- or, alternatively
-- ccatch = catchEPC
-- (>>) in index `e`
orElse :: ConjoinedMonads m => m e a -> m f a -> m f a
orElse f g = f `ccatch` const g
#+END_SRC
#+END_proof
A curious consequence of the above theorem and symmetries noted in~\cref{sec:logical} is that src_haskell{(>>=)} of src_haskell{EParser} of \cref{sec:parser-combinators:with-access} also has a roll-back version which satisfies src_haskell{Monad} laws
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
bindEP p f = EParser $ \s ->
case runEParser p s of
Left x -> Left x
Right (a, _) -> runEParser (f a) s
#+END_SRC
Though, of course, a src_haskell{EParser} that would use src_haskell{bindEP} in place of the usual src_haskell{(>>=)} could not be called a "parser" anymore.
Finally, note that src_haskell{(<|>)} operators of the src_haskell{Alternative} of \cref{sec:parser-combinators} for both src_haskell{SParser} and src_haskell{EParser} can be expressed in terms of their respective src_haskell{(>>=)} operators for their src_haskell{Monad}s in index src_haskell{e}
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
f `altSP'` g = f `catchSP` \e ->
g `catchSP` \e' ->
throwSP (e `mappend` e')
-- == (<|>)
f `altEPR'` g = f `catchEPR` \e ->
g `catchEPR` \e' ->
throwEP (e `mappend` e')
-- == altEPR
f `altEPC'` g = f `catchEPC` \e ->
g `catchEPC` \e' ->
throwEP (e `mappend` e')
-- == altEPC
#+END_SRC
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
instance Monoid e => Alternative (SParser s e) where
empty = SParser $ \_ -> Left mempty
(<|>) = altSP'
instance Monoid e => Alternative (EParser s e) where
empty = EParser $ \s -> Left (mempty, s)
(<|>) = altEPR'
-- or, when `ccatch == catchEPC`
-- (<|>) = altEPC'
#+END_SRC
**** The Interesting Part
@@tex:\label{sec:instances:parser-combinators:interesting}@@
The interesting part comes from the observation that src_haskell{some} and src_haskell{many} operators of src_haskell{Alternative} (\cref{sec:alternative}) never use the src_haskell{Monoid}al src_haskell{mappend}ing the above definitions of src_haskell{(<|>)} do, since both operators stop on the very first failure.
In other words, src_haskell{orElse}, which is just src_haskell{(>>)} operator for the src_haskell{Monad} in index src_haskell{e} (see above), is enough to implement them.
Interestingly, however, using src_haskell{orElse} instead of src_haskell{(<|>)} produces a curious effect of supplying these implementations with types that clearly show that src_haskell{some} inherits errors produced by its argument while src_haskell{many} ignores them
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
csome :: (ConjoinedMonads m, Applicative (m e))
=> m e a -> m e [a]
csome p = fmap (:) p <*> cmany p
cmany :: (ConjoinedMonads m, Applicative (m e))
=> m e a -> m f [a]
cmany p = csome p `orElse` cpure []
#+END_SRC
(In the above, src_haskell{Applicative} constraint is superfluous, it is an artifact or our encoding of src_haskell{ConjoinedMonads} into Haskell discussed in \cref{sec:encodings}.
We could elide it if we were to derive src_haskell{(<*>)} and src_haskell{fmap} operators from src_haskell{ConjoinedMonads}, an approach that we shall use in \cref{sec:pim:examples}.)
This method of substituting src_haskell{(<|>)} with src_haskell{orElse} extends to other similar combinators like src_haskell{choice}, src_haskell{optional}, src_haskell{sepBy}, 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.
*** 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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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}
#+BEGIN_SRC haskell :tangle TngEmeMain.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 TngEmeMain.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}.
#+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 TngEmeMain.hs
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) => ConjoinedMonads (ThrowT r m) where
cpure = pure
cbind = (>>=)
cthrow = throwT
ccatch = catchT
-- and similarly for `ThrowT'`
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
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
instance (Monad m) => ConjoinedMonads (ThrowT' m) where
cpure = pure
cbind = (>>=)
cthrow = throwT'
ccatch = catchT'
-- 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
#+END_SRC
#+END_proof
*** 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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.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 TngEmeMain.hs
instance ConjoinedMonads EIO where
cpure = pure
cbind = (>>=)
cthrow = throwEIO
ccatch = catchEIO
instance ConjoinedMonads SEIO where
cpure = pure
cbind = (>>=)
cthrow = throwSEIO
ccatch = catchSEIO
#+END_SRC
#+END_proof
*** 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{handleOrThrowAgain} 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}).
** Cartesian Products
@@tex:\label{sec:products}@@
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) -- `Monad` in `e`
, forall e . Monad (\a -> m e a)) -- `Monad` in `a`
=> 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 work 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 (\a -> m e a)
=> MonadXApplicative m where
#+END_SRC
In this structure the src_haskell{Monad}ic index gives 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, such a structure, at the very least, 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.
Moreover, since src_haskell{ConjoinedMonads} is a special case of src_haskell{MonadXApplicative}, all src_haskell{ConjoinedMonads} instances from the previous sections can also be used as a basis for such a formalism.
However, there are some interesting instances of src_haskell{MonadXApplicative} that are not src_haskell{ConjoinedMonads}.
Therefore, the question of interaction laws for this structure is also rather interesting.
Consider a folklore example of an src_haskell{Applicative} that is not a src_haskell{Monad}: "computations collecting failures in a src_haskell{Monoid}" (we used the same idea in src_haskell{Alternative} instances of~\cref{sec:parser-combinators,sec:instances:parser-combinators}), which can be defined as follows
#+BEGIN_SRC haskell :tangle TngEmeMain.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 that this structure, like src_haskell{Either}, can also be made a src_haskell{Monad} in index src_haskell{e}
#+BEGIN_SRC haskell :tangle TngEmeMain.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 TngEmeMain.hs :exports none
instance Monoid e => Functor (EA e) where
fmap f a = pure f <*> a
#+END_SRC
\noindent but, unlike for src_haskell{Either}, from the two interaction laws of \cref{dfn:proper} only the
#+BEGIN_SRC haskell-spec
pure a `catch` f == pure a
#+END_SRC
\noindent survives.
The law for src_haskell{throw} for this structure, if we are hard-set to write it down, looks like this
#+BEGIN_SRC haskell-spec
f <*> throw e == throw e' where
e' == e'' `mappend` e, for some e''
#+END_SRC
For the similar reasons it is not immediately obvious how to make imprecise exceptions into an instance of src_haskell{MonadXApplicative} since
- they are non-deterministic, hence disobeying all naive laws for src_haskell{throw}, and
- imprecise src_haskell{throw} has a wrong type to be the identity element for src_haskell{catch} (see \cref{rem:io-two-kinds-of-exceptions}).
\noindent However, 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 shall 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} (with similarly complicated interaction laws for src_haskell{throw}).
In \cref{sec:ale} we shall see that some interesting parser-combinator-related structures can be expressed by generalizing the src_haskell{Applicative}.
Similarly, in \cref{sec:pim} we shall also see that even more interesting parser-combinator-related structures can be expressed by generalizing the src_haskell{Monad}.
Thus, in general, the main observation is the following: **a lot of interesting structures that involve error handling are Cartesian products of src_haskell{Applicative}, src_haskell{Monad}, and/or their generalizations, with interaction laws that vary on case-by-case basis**.
We shall return to this point numerous times.
** Discussion
@@tex:\label{sec:eme:discussion}@@
The author hopes that with this part of the work we pointed and then at least partially plugged an algebraic hole in the programming languages theory by showing that
- exception handling without dynamic dispatch is dual to dual to conventional src_haskell{Monad}ic sequential computation, and
- conventional computational formalisms with src_haskell{throw/try/catch}-exceptions are "conjoined" Cartesian products of pairs of src_haskell{Monad}s (or, less imperatively, src_haskell{Monad}s and src_haskell{Applicative}s).
In author's opinion, these facts make a lot of conventional programming "click into place" similarly to how plain src_haskell{Monad}s "click" imperative "semicolons".
Moreover, they provide 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 work.
Also note that everything in this part (as well as in the rest of the work), 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.
This observation makes all the usual arguments against using src_haskell{Monad}s for error handling rather moot.
- The problem of syntactic non-uniformness between pure computations, src_haskell{Applicative}s and src_haskell{Monad}s 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 lists[fn::
And, similarly, for src_haskell{Traversable} and so on.]
can be rewritten as
#+BEGIN_SRC haskell :tangle TngPrelude.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.
- 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} conjoined product.
In other words, a programming language that
- provides a primitive src_haskell{catch} operator that does no dynamic dispatch (or, alternatively, provides no builtin error handling at all),
- provides quasi-quoting/compiling to categories for generalized src_haskell{Applicative}s,
- distinguishes between src_haskell{IO}-effects and non-determinism,
- allows one to express Cartesian products of type classes, and, possibly,
- uses a graded src_haskell{MonadXApplicative} for a base type of computations
\noindent could 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.
* Transforming Trees with Generalized src_haskell{Applicative} Expressions
@@tex:\label{sec:ale}@@
#+BEGIN_SRC haskell :tangle TngTypes.hs :exports none
{-# LANGUAGE StandaloneDeriving #-}
module TngTypes where
#+END_SRC
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs :exports none
import Data.SafeCopy
import Control.Arrow (Arrow)
import TngTypes
#+END_SRC
#+BEGIN_SRC haskell :tangle TngIntroAeson.hs :exports none
{-# LANGUAGE OverloadedStrings #-}
import Data.Aeson hiding (FromJSON, ToJSON)
import Data.Aeson.Types (Parser)
import Control.Applicative (empty)
import TngTypes
#+END_SRC
#+BEGIN_SRC haskell :tangle TngAleMain.hs :exports none
module TngAleMain where
import Data.Monoid
import Data.List (foldl', intersperse)
-- import Data.ByteString (ByteString)
import TngTypes
#+END_SRC
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs :exports none
{-# LANGUAGE RankNTypes, TypeFamilies, AllowAmbiguousTypes, MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies, TypeSynonymInstances #-}
import TngTypes
import TngAleMain
#+END_SRC
** Motivation
@@tex:\label{sec:ale:motivation}@@
Let us recall the definition of src_haskell{Applicative} type class~\cite{mcbride-paterson-08} (\cref{sec:applicative-functor}) as it is currently defined in the =base=~\cite{Hackage:base4900} package of Hackage~\cite{Hackage}
#+BEGIN_SRC haskell-spec
infixl 4 <*>
class Functor f => Applicative f where
pure :: a -> f a
(<*>) :: f (a -> b) -> f a -> f b
#+END_SRC
One can think of the above definition as simply providing a generic "constant injector" src_haskell{pure} and a somewhat generic "function application" src_haskell{(<*>)} operator.
(The referenced src_haskell{Functor} type class and any related algebraic laws can be completely ignored for the purposes of this part of the work.)
For instance, an identity on Haskell types is obviously an src_haskell{Applicative} with src_haskell{pure = id} and src_haskell{(<*>)} being the conventional function application (the one that is usually denoted by simple juxtaposition of terms), but there are many more complex instances of this type class (see \cref{sec:not-tutorial:basic,sec:not-tutorial:non-basic}, and~\cite{HaskellWiki:Typeclassopedia}), most (for the purposes of this work) notably, including src_haskell{Applicative} parser combinators.
Those are very popular in practice as they simplify parsing of simple data types ("simple" in this context means "without any type or data dependencies between different parts") to the point of triviality.
For instance, given appropriate src_haskell{Applicative} parsing machinery like Parsec~\cite{Hackage:parsec3111}, Attoparsec~\cite{Hackage:attoparsec01310} or Megaparsec~\cite{Hackage:megaparsec630} one can parse a simple data type like
#+BEGIN_SRC haskell :tangle TngTypes.hs
data Device = Device
{ block :: Bool
, major :: Int
, minor :: Int }
exampleDevice :: Device
exampleDevice = Device False 19 1
#+END_SRC
#+BEGIN_SRC haskell :tangle TngTypes.hs :exports none
deriving instance Show Device
#+END_SRC
\noindent from a straightforward serialized representation with just
#+BEGIN_SRC haskell-spec
class Parsable a where
parse :: Parser a
instance Parsable Device where
parse = pure Device <*> parse <*> parse <*> parse
#+END_SRC
While clearly limited to simple data types of a single[fn::Two or more constructors can be handled with the help of src_haskell{Alternative} type class and some tagging of choices.] constructor, this approach is very useful in practice.
Firstly, since these kinds of expressions make no variable bindings and all they do is repeatedly apply src_haskell{parse} it is virtually impossible to make a mistake.
Secondly, for the same reason it is exceptionally easy to generate such expressions via Template Haskell and similar metaprogramming mechanisms.
Which is why a plethora of Hackage libraries use this approach.
In this part we shall demonstrate a surprisingly simple technique that can be used to make computations expressing arbitrary transformations between simple data types of a single constructor (which, in particular, is rather useful for expressing isomorphisms and automorphisms of such types~\cite{Soloviev:2019:ATT}) while keeping the general form of src_haskell{Applicative} expressions as they were shown above.
Since we design our expressions to look similar to those produced with the help of src_haskell{Applicative} type class but the underlying structure is not src_haskell{Applicative} we shall call them "src_haskell{Applicative}-like".
\Cref{sec:motivating-examples} provides some motivating examples that show why we want to use src_haskell{Applicative}-like computations to express transformations between data types.
\Cref{sec:definition} formalizes the notion of "src_haskell{Applicative}-like" and discusses the properties we expect from such expressions.
\Cref{sec:deriving-the-technique} derives one particular structure for one of the motivating examples using LISP-encoding for deconstructing data types.
\Cref{sec:implementation} proceeds to derive the rest of motivating examples by applying the same idea, thus showing that \cref{sec:deriving-the-technique} describes a technique, not an isolated example.
\Cref{sec:implementation} ends by demonstrating the total expressive power of the technique.
\Cref{sec:scott} repeats the derivation and the implementations for Scott-encoded data types.
\Cref{sec:general-case} observes the general structure behind all of the terms used in the document.
\Cref{sec:formally} gives a formal description of the technique and the underlying general algebraic structure.
\Cref{sec:ale:products} shows how this technique can be combined with src_haskell{Monad}ic error handling of \cref{sec:eme}.
\Cref{sec:ale:discussion} discusses the consequences and the general picture.
*** Motivating Examples
@@tex:\label{sec:motivating-examples}@@
Consider the following expressions produced with the help of first author's favorite =safecopy=~\cite{Hackage:safecopy0943} data-type-to-binary serialization-deserialization library which can be used to deserialize-serialize src_haskell{Device} with the following code snippet (simplified[fn::The actual working code for the actual library looks a bit more complex, but the =safecopy= library also provides Template Haskell functions that derive these src_haskell{SafeCopy} instances automatically, so, in practice, one would not need to write this code by hand in any case.])
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
instance SafeCopy Device where
getCopy = pure Device <*> getCopy <*> getCopy <*> getCopy
putCopy (Device b x y) = putCopy b >> putCopy x >> putCopy y
#+END_SRC
Note that while src_haskell{getCopy} definition above is trivial, src_haskell{putCopy} definition binds variables.
Would not it be better if we had an src_haskell{Applicative}-like machinery with which we could rewrite src_haskell{putCopy} into something like
#+BEGIN_SRC haskell-spec
putCopy = depure unDevice <**> putCopy <**> putCopy <**> putCopy
#+END_SRC
\noindent which, incidentally, would also allow us to generate both functions from a single expression?
This idea does not feel like a big stretch of imagination for several reasons:
- there are libraries that can do both parsing and pretty printing using a single expression, e.g.~\cite{Hackage:syntax1000},
- the general pattern of src_haskell{putCopy} feels very similar to computations in src_haskell{(->) a} (the type of "functions from src_haskell{a}") as it, too, is a kind of computation in a context with a constant value, aka src_haskell{Reader} src_haskell{Monad}~\cite{Hackage:transformers0520}, which is an instance of src_haskell{Applicative}.[fn::@@tex:\label{fn:function-reader}@@We shall utilize this fact in the following sections.]
Another example is the data-type-to-JSON-to-strings serialization-deserialization part of =aeson=~\cite{Hackage:aeson1420} library which gives the following class signatures to its deserializer and serializer from/to JSON respectively.
#+BEGIN_SRC haskell :tangle TngIntroAeson.hs
class FromJSON a where
parseJSON :: Value -> Parser a
class ToJSON a where
toJSON :: a -> Value
#+END_SRC
In the above, src_haskell{Value} is a JSON value and src_haskell{Parser a} is a Scott-transformed variation of src_haskell{Either ErrorMessage a}.
Assuming src_haskell{(.:)} to be a syntax sugar for src_haskell{lookup}-in-a-map-by-name function and src_haskell{(.=)} a pair constructor, we can give the following instances for the src_haskell{Device} data type by emulating examples given in the package's own documentation
#+BEGIN_SRC haskell :tangle TngIntroAeson.hs
instance FromJSON Device where
parseJSON (Object v) = pure Device
<*> v .: "block"
<*> v .: "major"
<*> v .: "minor"
parseJSON _ = empty
instance ToJSON Device where
toJSON (Device b x y) = object
[ "block" .= b
, "major" .= x
, "minor" .= y ]
#+END_SRC
Note that here, again, we have to bind variables in src_haskell{toJSON}.
Moreover, note that in this example even src_haskell{parseJSON} underuses the src_haskell{Applicative} structure by ignoring the fact that src_haskell{Value} can be packed into src_haskell{Parser} by making the latter into a src_haskell{Reader}.[fn::
As noted under footnote~\ref{fn:function-reader} and demonstrated in detail in \cref{sec:deriving-the-technique}.
However, this underuse has a reasonable explanation for =aeson=: src_haskell{Value}'s definition is /too structured/ to have a conventional parser combinator library that can make this trick work in the general case (i.e. not just in the above example).
This problem can be solved using indexed src_haskell{Monad}ic parser combinators discussed in \cref{sec:pim}.]
Other serialization-deserialization problems, e.g. conventional pretty-printing with the standard src_haskell{Show} type class~\cite{Hackage:base4900} are, of course, the instances of the same pattern, as we shall demonstrate in the following sections.
Finally, as a bit more involved example, imagine an application that benchmarks some other software applications on given inputs, records logs they produce and then computes per-application averages
#+BEGIN_SRC haskell :tangle TngTypes.hs
data Benchmark a = Benchmark
{ firstApp :: a
, firstLog :: String
, secondApp :: a
, secondLog :: String
}
type Argv = [String]
type Inputs = Benchmark Argv
type Outputs = Benchmark Integer
type Avgs = Benchmark Double
#+END_SRC
#+BEGIN_SRC haskell :tangle TngAleMain.hs
benchmark :: Inputs -> IO Outputs
average :: [ Outputs ] -> Avgs
#+END_SRC
#+BEGIN_SRC haskell :tangle TngAleMain.hs :exports none
benchmark = undefined
#+END_SRC
Assuming that we have aforementioned machinery for src_haskell{SafeCopy} we can trivially autogenerate all of the needed glue code to deserialize src_haskell{Inputs}, serialize src_haskell{Outputs} and src_haskell{Avgs}.
The src_haskell{benchmark} is the core of our application, so let us assume that it is not trivial to autogenerate and we have to write it by hand.
We are now left with the src_haskell{average} function.
Let us assume that for the numeric parts of the src_haskell{Outputs} type it is just a src_haskell{fold} with point-wise sum over the list of src_haskell{Outputs} followed by a point-wise divide by their src_haskell{length} and for the src_haskell{String} parts it simply point-wise concatenates all the logs.
Now, do we really want to write those binary operators completely by hand?
Note that this src_haskell{Benchmark} example was carefully crafted: it is not self- or mutually-recursive and, at the same time, it is also not particularly homogeneous as different fields require different operations.
In other words, things like SYB~\cite{Laemmel:2003:SYB}, Uniplate~\cite{Mitchell:2007:Uniplate}, Multiplate~\cite{Hackage:multiplate003} or Lenses~\cite{Kmett:Lens, Hackage:lens417} are not particularly useful in this case.[fn::Strictly speaking, both operations used in the "sum" part of src_haskell{average} are src_haskell{Monoid} operators, so generalized src_haskell{zip}s provided by some of the mentioned libraries can be used to implement that part, but the "divide" part is not so homogeneous.]
Of course, in this particular example, it is possible to distill the computation pattern into something like
#+BEGIN_SRC haskell :tangle TngAleMain.hs
lift2B :: (a -> b -> c) -> (Benchmark a -> Benchmark b -> Benchmark c)
lift2B f (Benchmark a1 l1 a2 l2) (Benchmark b1 l3 b2 l4)
= Benchmark (f a1 b1) (l1 ++ l3) (f a2 b2) (l2 ++ l4)
#+END_SRC
\noindent and then use src_haskell{lift2B} to implement both functions (with some unsightly hackery for the division part), but would not it be even better if instead we had an src_haskell{Applicative}-like machinery that would allow us to write the src_haskell{average} function directly, such as
#+BEGIN_SRC haskell :tangle TngAleMain.hs
average ls = runMap $ bdivide folded where
len = fromIntegral $ length ls
avg = (/ len) . fromIntegral
bappend = depureZip Benchmark unBenchmark unBenchmark
`zipa` (+) `zipa` (++)
`zipa` (+) `zipa` (++)
folded = foldl' (\a b -> runZip $ bappend a b)
(Benchmark 0 "" 0 "") ls
bdivide = depureMap Benchmark unBenchmark
`mapa` avg `mapa` id
`mapa` avg `mapa` id
#+END_SRC
\noindent similarly to how we would solve similar problems over homogeneous lists?
** Derivation
*** Problem Definition
@@tex:\label{sec:definition}@@
Before going into derivation of the actual implementation let us describe what we mean by "src_haskell{Applicative}-like" more precisely.
Note that the type of src_haskell{(<*>)} operator of src_haskell{Applicative}
#+BEGIN_SRC haskell-spec
(<*>) :: f (a -> b) -> f a -> f b
#+END_SRC
\noindent at least in the context of constructing data types (of which src_haskell{Applicative} parsers are a prime example), can be generalized and reinterpreted as
#+BEGIN_SRC haskell-spec
plug :: f full -> g piece -> f fullWithoutThePiece
#+END_SRC
\noindent where
- src_haskell{f full} is a computation that /provides a mechanism/ to handle the src_haskell{full} structure,
- src_haskell{g piece} is another kind of computation that /actually handles/ a src_haskell{piece} of the src_haskell{full} structure (src_haskell{g == f} for src_haskell{Applicative} parsers, of course),
- and src_haskell{f fullWithoutThePiece} is a computation that provided a mechanism to handle the leftover part.
Note that this interpretation, in some sense, reverses conventional wisdom on how such transformations are usually expressed.
For instance, conventionally, to parse (pretty-print, etc) some structure one first makes up computations that handle src_haskell{piece}s and then composes them into a computation that handles the src_haskell{full} structure, i.e.
#+BEGIN_SRC haskell-spec
compose :: f fullWithoutThePiece -> g piece -> f full
-- or
compose' :: g piece -> f fullWithoutThePiece -> f full
#+END_SRC
Meanwhile, src_haskell{Applicative}-like expressions, in some sense, work backwards: they provide a mechanism to handle (parse, pretty-print, etc) the src_haskell{full} structure that exposes "ports" that subcomputations src_haskell{plug} with computations that handle different src_haskell{piece}s.
#+BEGIN_remark
It is rather interesting to think about the conventional function application in these terms: it describes a way to make a computation that produces src_haskell{b} given a mechanism to construct a partial version of src_haskell{b} denoted as src_haskell{a -> b} by plugging its only port with a computation that produces src_haskell{a}.
In other words, this outlook is a reminder that functions can be seen as goals, the same way Haskell's type class instance inference (or Prolog) does.
Moreover, note that while such a description sounds obvious for a lazy language, it is also a reminder that, in general, there is a distinction between values and computations.
#+END_remark
To summarize, the crucial part of src_haskell{Applicative}-like computations is the fact that they compose subcomputations in reverse order w.r.t. the types they handle.
This reversal is the cornerstone that provides three important properties:
- A sequence of subcomputations in an expression matches the sequence of parts in the corresponding data type.
- A top-level computation can decide on all data types /first/ and then delegate handing of parts to subcomputations without worrying about reassembling their results (which is why we say it "provides a mechanism" that subcomputations use).
- As a consequence, in the presence of type inference, a mechanism for ad-hoc polymorphism (be it type classes, like in Haskell, or something else) can be used to automatically select implementations matching corresponding src_haskell{piece}s.
It is the combination of these three properties that makes src_haskell{Applicative}-like expressions (including src_haskell{Applicative} parsers) so convenient in practice.
*** Deriving the Technique
@@tex:\label{sec:deriving-the-technique}@@
We shall now demonstrate the derivation of the main technique of the document.
Before we start, let us encode reverses to src_haskell{Device} and src_haskell{Benchmark} constructors (i.e. "destructors") using the LISP-encoding (see below for motivation, an alternative approach using Scott-encoding is discussed in section~\ref{sec:scott}).
#+BEGIN_SRC haskell :tangle TngTypes.hs
unDeviceLISP :: Device -> (Bool, (Int, (Int, ())))
unDeviceLISP (Device b x y) = (b, (x, (y, ())))
unBenchmarkLISP :: Benchmark a -> (a, (String, (a, (String, ()))))
unBenchmarkLISP (Benchmark a b c d) = (a, (b, (c, (d, ()))))
#+END_SRC
Now, let us start by deriving an src_haskell{Applicative}-like pretty-printer for src_haskell{Device}.
The target expression is as follows
#+BEGIN_SRC haskell :tangle TngAleMain.hs
showDevice = depureShow unDeviceLISP `showa` show
`showa` show
`showa` show
#+END_SRC
Remember that the type pattern for the src_haskell{plug} operator from the previous section
#+BEGIN_SRC haskell-spec
plug :: f full -> g piece -> f fullWithoutThePiece
#+END_SRC
\noindent already prescribes a certain way of implementing the missing operators.
Firstly, if we follow the logic for parsing, the src_haskell{f} type-level function should construct a type that contains some internal state.
Secondly, the rest of the expression clearly requires src_haskell{depureShow} to generate the initial state and src_haskell{showa} to transform the internal state while chopping away at the parts of the src_haskell{Device}.
Let us simplify the task of deriving these functions by writing out the desired type and making src_haskell{Device} argument explicit.
Let us also apply the result of the whole computation to src_haskell{runShow} function to lift the restriction on the return type.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
showDevice' :: Device -> String
showDevice' d = runShow $ depureShow' (unDeviceLISP d) `showa'` show
`showa'` show
`showa'` show
#+END_SRC
What should be the type of src_haskell{showa'}? Clearly, something like
#+BEGIN_SRC haskell-spec
showa' :: (s, (a, b)) -> (a -> String) -> (s, b)
#+END_SRC
\noindent should work and match the type pattern of src_haskell{plug}.
The src_haskell{a -> String} part follows from the expression itself, the src_haskell{(_ , (a, b))} and src_haskell{(_ , b)} parts come from chopping away at LISP-encoded deconstructed data type, and src_haskell{s} plays the role of the internal pretty-printing state.
We just need to decide on the value of src_haskell{s}.
The most simple option seems to be to the list of src_haskell{String}s that is to be concatenated in src_haskell{runShow}.
The rest of the code pretty much writes itself:
#+BEGIN_SRC haskell :tangle TngAleMain.hs
depureShow' :: a -> ([String], a)
depureShow' a = ([], a)
showa' :: ([String], (a, b)) -> (a -> String) -> ([String], b)
showa' (s, (a, b)) f = ((f a):s, b)
runShow :: ([String], b) -> String
runShow = concat . intersperse " " . reverse . fst
testShowDevice' :: String
testShowDevice' = showDevice' exampleDevice
-- == "False 19 1"
#+END_SRC
Now, note that src_haskell{showa'} is actually a particular case of the more generic operator
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chop :: (s, (a, b)) -> (s -> a -> t) -> (t, b)
chop (s, (a, b)) f = (f s a, b)
showa'' s f = chop s (\s a -> (f a):s) -- == showa'
#+END_SRC
Moreover, src_haskell{f} parts of that operator can be wrapped into the src_haskell{(->) r} src_haskell{Reader} (remember footnote~\ref{fn:function-reader})
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chopR :: (r -> (s, (a, b))) -> (s -> a -> t) -> (r -> (t, b))
chopR o f r = chop (o r) f
#+END_SRC
\noindent thus allowing us to complete the original
src_haskell{showDevice}
#+BEGIN_SRC haskell :tangle TngAleMain.hs
showDevice :: Device -> ([String], ())
depureShow :: (r -> b) -> r -> ([String], b)
depureShow f r = ([], f r)
showa :: (r -> ([String], (a, b)))
-> (a -> String)
-> (r -> ([String], b))
showa st f = chopR st (\s a -> (f a):s)
testShowDevice :: String
testShowDevice = runShow $ showDevice exampleDevice
-- == "False 19 1"
#+END_SRC
Note that the use of the LISP-encoding (i.e. the src_haskell{()} in the tails of the deconstructed types and, hence, the use of src_haskell{fst} in src_haskell{runShow}) as opposed to using simple stacked tuples is needed to prevent special case handling for the last argument.
Also note that the type of the second argument to src_haskell{chopR} in the definition of src_haskell{showa} is src_haskell{[String] -> a -> [String]} which is src_haskell{CoState} on a list of src_haskell{String}s.
This makes a lot of sense categorically since src_haskell{Parser} is a kind of src_haskell{State} and parsing and pretty-printing are dual.
Moreover, even the fact that src_haskell{String} is wrapped into a list makes sense if one is to note that the above pretty-printer produces /lexemes/ instead of directly producing the output string.
The above transformation from src_haskell{chop} to src_haskell{chopR} will be a common theme in the following sections, so let us distill it into a separate operator with a very self-descriptive type
#+BEGIN_SRC haskell :tangle TngAleMain.hs
homWrap :: (s -> a -> t)
-> (r -> s) -> a -> (r -> t)
homWrap chopper o f r = chopper (o r) f
showa''' = homWrap $ \st f -> chop st $ \s a -> (f a):s -- == showa
#+END_SRC
*** Applying the Technique
@@tex:\label{sec:implementation}@@
Turning attention back to src_haskell{chop} operator, note that both types in the state tuple can be arbitrary.
For instance, src_haskell{s} can be a curried data type constructor, which immediately allows to express an src_haskell{Applicative}-like step-by-step equivalent of src_haskell{map}.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
mapa :: (r -> (x -> y, (a, b)))
-> (a -> x)
-> (r -> (y, b))
mapa = homWrap $ \st f -> chop st $ \s a -> s (f a)
depureMap :: a -> (r -> b) -> r -> (a, b)
depureMap c f r = (c, f r)
runMap = fst
mapDevice :: Device -> (Device, ())
mapDevice = depureMap Device unDeviceLISP
`mapa` not
`mapa` (+ 100)
`mapa` (+ 200)
testMapDevice :: Device
testMapDevice = runMap $ mapDevice exampleDevice
-- == Device True 119 201
#+END_SRC
Moreover, by extending src_haskell{chop} with two LISP-encoded representations and repeating the whole derivation we can express an equivalent of src_haskell{zip}.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chop2 :: (s, (a, b), (c, d))
-> (s -> a -> c -> t)
-> (t, b, d)
chop2 (s, (a, b), (c, d)) f = (f s a c, b, d)
homWrap2 chopper o f ra rb = chopper (o ra rb) f
zipa :: (ra -> rb -> (x -> y, (a, b), (c, d)))
-> (a -> c -> x)
-> (ra -> rb -> (y, b, d))
zipa = homWrap2 $ \st f -> chop2 st $ \s a b -> s (f a b)
depureZip :: a -> (ra -> b) -> (rb -> c)
-> ra -> rb
-> (a, b, c)
depureZip c f g ra rb = (c, f ra, g rb)
runZip :: (s, a, b) -> s
runZip (s, _, _) = s
zipDevice :: Device -> Device -> (Device, (), ())
zipDevice = depureZip Device unDeviceLISP unDeviceLISP
`zipa` (&&)
`zipa` (+)
`zipa` (+)
testZipDevice :: Device
testZipDevice = runZip $ zipDevice exampleDevice testMapDevice
-- == Device False 138 202
#+END_SRC
The above transformations combined with
#+BEGIN_SRC haskell :tangle TngTypes.hs
unDevice = unDeviceLISP
unBenchmark = unBenchmarkLISP
#+END_SRC
\noindent implement all the examples from \cref{sec:motivating-examples}, thus solving the problem as it was originally described.
Note, however, that the above technique can be trivially extended to src_haskell{chop}ping any number of data types at the same time and, moreover, that it is not actually required to match types or even the numbers of arguments of different constructors and destructors used by the desired transformations.
For instance, it is trivial to implement the usual stack machine operators, e.g.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
homWrap0 :: (s -> t)
-> (r -> s) -> (r -> t)
homWrap0 chopper o r = chopper (o r)
-- syntax sugar
andThen x f = f x
pop :: (r -> (s, (a, b)))
-> (r -> (s, b))
pop = homWrap0 $ \(s, (_, b)) -> (s, b)
push = homWrap $ \(s, b) a -> (s, (a, b))
dup = homWrap0 $ \(s, (a, b)) -> (s, (a, (a, b)))
#+END_SRC
\noindent and use them to express some mapping function between data types as if Haskell was a stack machine language
#+BEGIN_SRC haskell :tangle TngAleMain.hs
remapDevice :: Device -> (Device, ())
remapDevice = depureMap Device unDeviceLISP
`andThen` pop
`push` True
`mapa` id
`andThen` pop
`andThen` dup
`mapa` id
`mapa` id
testRemapDevice :: Device
testRemapDevice = runMap $ remapDevice exampleDevice
-- == Device True 1 1
#+END_SRC
In other words, in general, one can view src_haskell{Applicative}-like computations as computations for generalized multi-stack machines with arbitrary data types and/or functions as "stacks".
In practice, though, simple direct transformations in the style of src_haskell{Applicative} parsers seem to be the most useful use case.
*** Scott-encoded Representation
@@tex:\label{sec:scott}@@
The LISP-encoding used above is not the only generic representation for data types, in this section we shall repeat the above results for Scott-encoded data types.
Before we start, let us note that while it is trivial to simply Scott-encode all the pair constructors and destructors in the above transformations to get more complicated terms with exactly equivalent semantics (see \cref{sec:scott-encoding}), it just complicates things structurally, and we shall not explore that route.
The interesting question is whether it is possible to remake the above machinery directly for Scott-encoded representations of the subject data types
#+BEGIN_SRC haskell :tangle TngTypes.hs
unDeviceScott :: Device -> (Bool -> Int -> Int -> c) -> c
unDeviceScott (Device b x y) f = f b x y
unBenchmarkScott :: Benchmark a
-> (a -> String -> a -> String -> c) -> c
unBenchmarkScott (Benchmark a b c d) f = f a b c d
#+END_SRC
\noindent without reaching for anything else.
In other words, would not it be nice if we could work with a Scott-encoded data type src_haskell{(a -> b -> c -> ... -> z) -> z} as if it was a heterogeneous list of typed values like LISP-encoding is?
Let us start by noticing that we can, in fact, prepend values to Scott-encoded representations as if they were heterogeneous lists or tuples
#+BEGIN_SRC haskell :tangle TngAleMain.hs
consS :: s
-> (a -> b)
-> ((s -> a) -> b)
consS s ab sa = ab (sa s)
#+END_SRC
To see why this prepends src_haskell{s} to a Scott-encoded src_haskell{a -> b} substitute, for instance, src_haskell{x -> y -> b} for src_haskell{a}.
Note, however, that there are some important differences.
For instance, Scott-encoded data types, unlike LISP-encoded ones, can not have a generic src_haskell{unconsS}
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
unconsS :: ((s -> a) -> b) -> (s, a -> b)
unconsS f = (_, _)
#+END_SRC
\noindent as, in general, all the pieces of a Scott-encoded data type have to be used all at once.
This makes most of our previous derivations unusable.
However, very surprisingly, src_haskell{consS} seems to be enough.
By prepending src_haskell{s} to the Scott-encoded data type we can emulate pretty-printing code above as follows.[fn::We tried our best to make this comprehensible by making the types speak for themselves but, arguably, this and the following listings can only be really understood by playing with the Literate Haskell version in =ghci=.]
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chopS :: ((s -> a -> b) -> c)
-> (s -> a -> t)
-> ((t -> b) -> c)
chopS i f o = i $ \s a -> o (f s a)
depureShowS f r = consS [] (f r)
showaS :: (r -> ([String] -> a -> b) -> c)
-> (a -> String)
-> (r -> ([String] -> b) -> c)
showaS = homWrap $ \st f -> chopS st $ \s a -> (f a):s
runShowS = concat . intersperse " " . reverse . (\f -> f id)
showDeviceS = depureShowS unDeviceScott
`showaS` show
`showaS` show
`showaS` show
testShowDeviceS = runShowS $ showDeviceS exampleDevice
-- == testShowDevice
#+END_SRC
The only new parts here are the implementation of src_haskell{chopS} function, the use of src_haskell{consS} instead of the pair constructor, and the replacement of src_haskell{fst} with src_haskell{\f -> f id}.
The rest is produced mechanically by adding =S= suffix to all function calls.
The src_haskell{map} example can be similarly mechanically translated as follows.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
mapaS :: (r -> ((x -> y) -> a -> b) -> c)
-> (a -> x)
-> (r -> (y -> b) -> c)
mapaS = homWrap $ \st f -> chopS st $ \s a -> s (f a)
depureMapS c f r = consS c (f r)
runMapS f = f id
mapDeviceS = depureMapS Device unDeviceScott
`mapaS` not
`mapaS` (+ 100)
`mapaS` (+ 200)
testMapDeviceS :: Device
testMapDeviceS = runMapS $ mapDeviceS exampleDevice
-- == testMapDevice
#+END_SRC
The most interesting part, however, is the reimplementation of src_haskell{zip}.
By following the terms in the previous section we would arrive at the following translation for src_haskell{depureZip}
#+BEGIN_SRC haskell :tangle TngAleMain.hs
depureZipS' :: s -> (ra -> a) -> (rb -> b -> c)
-> ra -> rb
-> (s -> a -> b) -> c
depureZipS' c f g r s = consS c (consS (f r) (g s))
#+END_SRC
\noindent Frustratingly, there is no src_haskell{chop2} equivalent for it
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
chop2S' :: ((s -> ((a -> b) -> c) -> d -> e) -> f)
-> (s -> a -> d -> t)
-> (t -> (b -> c) -> e) -> f
chop2S' i f o = i $ \s abq d -> o _ _
#+END_SRC
\noindent because src_haskell{a} becomes effectively inaccessible in this order of src_haskell{consS}ing (as there is no src_haskell{unconsS}).
However, fascinatingly, by simply changing that order to
#+BEGIN_SRC haskell :tangle TngAleMain.hs
depureZipS c f g r s = consS (consS c (f r)) (g s)
#+END_SRC
\noindent we get our src_haskell{cons2S} and, by mechanical translation, all the rest of src_haskell{zipDevice} example
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chop2S :: ((((s -> a -> b) -> c) -> d -> e) -> f)
-> (s -> a -> d -> t)
-> (((t -> b) -> c) -> e) -> f
chop2S i f o = i $ \sabc d -> o $ \tb -> sabc $ \s a -> tb $ f s a d
zipaS :: (ra -> rb -> (((((x -> y) -> a -> b) -> c) -> d -> e) -> f))
-> (a -> d -> x)
-> (ra -> rb -> (((y -> b) -> c) -> e) -> f)
zipaS = homWrap2 $ \st f -> chop2S st $ \s a b -> s (f a b)
runZipS f = f id id
zipDeviceS = depureZipS Device unDeviceScott unDeviceScott
`zipaS` (&&)
`zipaS` (+)
`zipaS` (+)
testZipDeviceS :: Device
testZipDeviceS = runZipS $ zipDeviceS exampleDevice testMapDeviceS
-- == testZipDevice
#+END_SRC
\noindent thus, again, implementing all the examples from \cref{sec:motivating-examples}, but now purely with Scott-encoded data types.
#+BEGIN_remark
Note that while the transformation from src_haskell{b} to src_haskell{(a, b)} for the LISP-encoding or the plain tuples is regular, the transformation from src_haskell{(a -> b -> c -> ... -> z) -> z} to src_haskell{(s -> a -> b -> c -> ... -> z) -> z} is not, the former is not a subexpression of the latter.
Taking that into account, the author feels that the very fact that the implementations demonstrated above are even possible is rather fascinating.
The fact that Scott-encoding can be used as a heterogeneous list is rather surprising as even the fact that src_haskell{consS} is possible is rather weird, not to mention the fact that useful things can be done without src_haskell{unconsS}.
We are not aware of any literature that describes similar transformations over Scott-encoded data types.
The closest works we are aware of that do vaguely related things with Scott-encoded values are~\cite{Rhiger:2009:TSP} and~\cite{Danvy:1998:FU} (though, neither explicitly mentions the fact).
#+END_remark
*** General Case
@@tex:\label{sec:general-case}@@
Curiously, note that with the aforementioned order of src_haskell{consS}ing src_haskell{chop2S} is actually a special case of src_haskell{chopS}
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chop2S' :: ((((s -> a -> b) -> c) -> d -> e) -> f)
-> (s -> a -> d -> t)
-> (((t -> b) -> c) -> e) -> f
chop2S' i f o = chopS i (\sabc d tb -> sabc $ \s a -> tb $ f s a d) o
-- == chop2S
#+END_SRC
\noindent and this pattern continues when src_haskell{consS}ing more structures
#+BEGIN_SRC haskell :tangle TngAleMain.hs
depureZip3S :: s -> (ra -> a -> b) -> (rb -> c -> d) -> (rc -> e -> f)
-> ra -> rb -> rc
-> (((((s -> a) -> b) -> c) -> d) -> e) -> f
depureZip3S c f g h r s t = consS (consS (consS c (f r)) (g s)) (h t)
chop3S :: ((((((s -> a -> b) -> c) -> d -> e) -> f) -> g -> h) -> i)
-> (s -> a -> d -> g -> t)
-> (((((t -> b) -> c) -> e) -> f) -> h) -> i
chop3S i f o = chop2S i (\sabc d g tb -> sabc $ \s a -> tb $ f s a d g) o
-- and so on
#+END_SRC
The same is true for LISP-encoded variant since we can use the same order of src_haskell{cons}ing there, e.g.
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chop2' :: ((s, (a, b)), (c, d))
-> (s -> a -> c -> t)
-> ((t, b), d)
chop2' (sab, (c, d)) f = (chop sab (\s a -> f s a c), d)
-- ~~ chop2
#+END_SRC
\noindent but we think this presentation makes things look more complex there, not less.
Though, as we shall see in the next section (in its Literal Haskell version), we could have simplified the general case by using src_haskell{chop2'} above.
In other words, if we are to src_haskell{cons} LISP-encoded and src_haskell{consS} Scott-encoded data types in the right order then all of the src_haskell{Applicative}-like operators of this document and the generalizations of src_haskell{Applicative}-like src_haskell{zip}s to larger numbers of structures can be uniformly produced from just src_haskell{chop} and src_haskell{chopS}.
*** Formal Account
@@tex:\label{sec:formally}@@
The derivation of \cref{sec:deriving-the-technique}, as demonstrated by the following sections, describes a technique (as opposed to an isolated example) for expressing transformations between simple data types of a single constructor using src_haskell{Applicative}-like computations.
More formally, that technique consists of
- deconstructing the data type (into its LISP-encoded representation in \cref{sec:deriving-the-technique,sec:implementation} or Scott-encoded representation in \cref{sec:scott}),
- wrapping the deconstructed representation into the src_haskell{Applicative}-like structure in question with an operation analogous to src_haskell{Applicative}'s src_haskell{pure} (src_haskell{depureShow}, etc),
- followed by spelling out transformation steps to the desired representation by interspersing them with an operator analogous to src_haskell{Applicative}'s src_haskell{(<*>)} (src_haskell{showa}, src_haskell{mapa}, src_haskell{zipa}, etc),
- followed by wrapping the whole structure into src_haskell{(->) r} src_haskell{Reader} that is used to propagate the input argument to the front of the expression without adding explicit argument bindings to the whole expressions.
Note, however, that the last "wrapping" bit of the translation is orthogonal to the rest.
It is needed to produce a completely variable-binding-less expression, but that step can be skipped if variable-binding-lessness is not desired: one simply needs to remove the src_haskell{homWrap} wrapping, add an explicitly bound argument to the function, and then apply it to src_haskell{depureShow}.
Also remember that \cref{sec:implementation} showed that, in general, those expressions can express arbitrary computations for generalized multi-stack machines with arbitrary data types and/or functions as "stacks".
For the src_haskell{show}-, src_haskell{map}-, and src_haskell{zip}-like transformations we described in detail, however, the central src_haskell{chop} operator corresponds to a simple state transformer of the corresponding "step-by-step" src_haskell{fold}, if we are to view the deconstructed data type as a heterogeneous list.
Finally, note that while src_haskell{depureMap} and src_haskell{depureZip} (src_haskell{depureMapS} and src_haskell{depureZipS}) take more arguments than src_haskell{Applicative}'s src_haskell{pure} this fact is actually inconsequential as in \cref{sec:general-case} we noted that we can simply reorganize all our expressions to src_haskell{cons} to the left (as we had to do for Scott-encoded data types).
Thus, only the last argument to the src_haskell{depure*} functions is of any consequence to the general structure (since it is the argument we are src_haskell{fold}ing on, inductively speaking), the rest are simply baggage used internally by the corresponding operators.
**** Dependently-typed src_haskell{Applicative}
@@tex:\label{sec:ale:deptypes}@@
Now, the obvious question is how a general structure unifying all those operators would look.
Firstly, remember that the src_haskell{pure} function of src_haskell{Applicative} can be separated out into its own type class (see \cref{sec:applicative-functor})
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.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
\noindent Moreover, note that, algebraically speaking, src_haskell{Applicative} depends on src_haskell{Pointed} only because their combination gives src_haskell{Functor}, they are independent otherwise.
Since we have no equivalent for src_haskell{Functor} with src_haskell{Applicative}-like expressions we can discuss these two parts separately.
Secondly, let us note that src_haskell{Control.Category} and src_haskell{Control.Arrow} modules of =base=~\cite{Hackage:base4900} define src_haskell{Category}~\cite{Hackage:base4900} and src_haskell{ArrowApply}~\cite{hughes-arrows-00} type classes as
#+BEGIN_SRC haskell :tangle TngSyntaxCheckOnly.hs
class Category cat where
id :: cat a a
(.) :: cat b c -> cat a b -> cat a c
class Arrow a => ArrowApply a where
app :: a (a b c, b) c
#+END_SRC
\noindent respectively.
Both of these type classes denote generalized functions over generalized function types: src_haskell{cat} and src_haskell{a} respectively.
Thirdly, if we are to look at the types of our src_haskell{showa}, src_haskell{mapa}, and src_haskell{zipa} operators and their versions for Scott-encoded data types, the most glaring difference from the type of src_haskell{(<*>)} we will notice is the fact that the types of their second arguments and the types of their results depend on the types of their first arguments (or, equivalently, we can say that all of those depend on another implicit type argument).
In other words, if src_haskell{(<*>)} and src_haskell{app} are two generalizations of the conventional function application, then the structure that describes our operators is a generalization of the dependently typed function application.
**** Haskell Encoding
@@tex:\label{sec:ale:encoding}@@
The simplest generic encoding we have for our examples for GHC Haskell (with awful lot of extensions) looks like this
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs
class ApplicativeLike f where
type C f a b :: * -- type of arrow under `f`
type G f a :: * -- type of argument dependent on `f`
type F f b :: * -- type of result dependent on `f`
(<**>) :: f (C f a b) -> G f a -> F f b
#+END_SRC
Note however, that since our analogues of src_haskell{pure} operator simply wrap results produced by the data type destructors into corresponding initial states, their generalization is not interesting (in general, it is a function src_haskell{a -> f b}).
Moreover, generalizing it actually adds problems because a generic src_haskell{depure} makes src_haskell{(<**>)} ambitious in
#+BEGIN_SRC haskell-spec
ambitiousExample a = depure unDevice <**> a <**> a <**> a
#+END_SRC
\noindent This does not happen for src_haskell{Applicative} type class since both arguments to src_haskell{(<*>)} are of the same type family src_haskell{f} there.
Thus, src_haskell{ApplicativeLike}, unlike src_haskell{Applicative}, should not be src_haskell{Pointed}.
The rest of the section demonstrates the use of the above generic encoding.
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs
newtype Mapper r f a = Mapper { runMapper :: r -> (f, a) }
instance ApplicativeLike (Mapper r (x -> y)) where
type C (Mapper r (x -> y)) a b = (a, b)
type G (Mapper r (x -> y)) a = a -> x
type F (Mapper r (x -> y)) b = Mapper r y b
f <**> g = Mapper $ mapa (runMapper f) g
mapDeviceG :: Mapper Device Device ()
mapDeviceG = Mapper (depureMap Device unDeviceLISP)
<**> not
<**> (+ 100)
<**> (+ 200)
testMapDeviceG :: Device
testMapDeviceG = runMap $ runMapper mapDeviceG exampleDevice
newtype MapperS c r f a = MapperS
{ runMapperS :: r -> (f -> a) -> c }
instance ApplicativeLike (MapperS c e (x -> y)) where
type C (MapperS c e (x -> y)) a b = a -> b
type G (MapperS c e (x -> y)) a = a -> x
type F (MapperS c e (x -> y)) b = MapperS c e y b
f <**> g = MapperS $ mapaS (runMapperS f) g
mapDeviceGS :: MapperS c Device Device c
mapDeviceGS = MapperS (depureMapS Device unDeviceScott)
<**> not
<**> (+ 100)
<**> (+ 200)
testMapDeviceGS :: Device
testMapDeviceGS = runMapS $ runMapperS mapDeviceGS exampleDevice
newtype Printer r a = Printer
{ runPrinter :: r -> ([String], a) }
instance ApplicativeLike (Printer e) where
type C (Printer e) a b = (a, b)
type G (Printer e) b = b -> String
type F (Printer e) b = Printer e b
f <**> g = Printer $ showa (runPrinter f) g
showDeviceG :: Printer Device ()
showDeviceG = Printer (depureShow unDeviceLISP)
<**> show
<**> show
<**> show
testShowDeviceG :: String
testShowDeviceG = runShow $ runPrinter showDeviceG exampleDevice
newtype PrinterS c r a = PrinterS
{ runPrinterS :: r -> ([String] -> a) -> c }
instance ApplicativeLike (PrinterS c e) where
type C (PrinterS c e) a b = a -> b
type G (PrinterS c e) a = a -> String
type F (PrinterS c e) b = PrinterS c e b
f <**> g = PrinterS $ showaS (runPrinterS f) g
showDeviceGS :: PrinterS c Device c
showDeviceGS = PrinterS (depureShowS unDeviceScott)
<**> show
<**> show
<**> show
testShowDeviceGS :: String
testShowDeviceGS = runShowS $ runPrinterS showDeviceGS exampleDevice
newtype Zipper ra rb f a = Zipper
{ runZipper :: ra -> rb -> (f, a) }
-- we need these, because we used tuples in `zipa`
toZipper f = Zipper $ \ra rb -> (\(a, b, c) -> ((a, b), c)) $ f ra rb
fromZipper f = \ra rb -> (\((a, b), c) -> (a, b, c)) $ runZipper f ra rb
instance ApplicativeLike (Zipper e e (x -> y, (a, b))) where
type C (Zipper e e (x -> y, (a, b))) c d = (c, d)
type G (Zipper e e (x -> y, (a, b))) c = a -> c -> x
type F (Zipper e e (x -> y, (a, b))) d = Zipper e e (y, b) d
f <**> g = toZipper $ zipa (fromZipper f) g
zipDeviceG :: Zipper Device Device (Device, ()) ()
zipDeviceG = toZipper (depureZip Device unDeviceLISP unDeviceLISP)
<**> (&&)
<**> (+)
<**> (+)
testZipDeviceG :: Device
testZipDeviceG = runZip $ (\((a, b), c) -> (a, b, c))
$ runZipper zipDeviceG exampleDevice testMapDeviceG
newtype ZipperS z z' ra rb f g a = ZipperS
{ runZipperS :: ra -> rb -> (((f -> g) -> z) -> a) -> z' }
instance ApplicativeLike (ZipperS z z' e e (x -> y) (a -> b)) where
type C (ZipperS z z' e e (x -> y) (a -> b)) c d = c -> d
type G (ZipperS z z' e e (x -> y) (a -> b)) c = a -> c -> x
type F (ZipperS z z' e e (x -> y) (a -> b)) d = ZipperS z z' e e y b d
f <**> g = ZipperS $ zipaS (runZipperS f) g
zipDeviceGS :: ZipperS z z' Device Device Device z z'
zipDeviceGS = ZipperS (depureZipS Device unDeviceScott unDeviceScott)
<**> (&&)
<**> (+)
<**> (+)
testZipDeviceGS :: Device
testZipDeviceGS = runZipS $ runZipperS zipDeviceGS exampleDevice testMapDeviceGS
#+END_SRC
** Cartesian Products
@@tex:\label{sec:ale:products}@@
If one is to take the src_haskell{ApplicativeLike} of \cref{sec:ale:encoding} seriously, that is, if one is to use src_haskell{(<**>)} as /the/ function application operator then, as noted in \cref{sec:products}, it would make a lot of sense to take a Cartesian product of src_haskell{Monad} with src_haskell{ApplicativeLike} to supply such a formalism with error handling operators.
To archive such a Cartesian product we just need to add another index signifying errors to our state transformer and use that index in a composition with something that is a src_haskell{Monad} in that index.
For instance, for LISP-encoded data types and src_haskell{Either} this gives us the following definition for the corresponding analogue of the src_haskell{chop} operator
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chopE' :: Either e (s, (a, b)) -> (s -> a -> Either e t) -> Either e (t, b)
chopE' (Left e) _ = Left e
chopE' (Right (s, (a, b))) f = case f s a of
Left e -> Left e
Right fsa -> Right (fsa, b)
#+END_SRC
\noindent or, alternatively, explicitly using the fact that src_haskell{Either} is a src_haskell{Monad}
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chopE :: Either e (s, (a, b)) -> (s -> a -> Either e t) -> Either e (t, b)
chopE i f = do
(s, (a, b)) <- i
fsa <- f s a
pure (fsa, b)
-- == chopE'
#+END_SRC
\noindent (note that src_haskell{chopE} is exactly the definition of src_haskell{chop} of \cref{sec:deriving-the-technique} with all src_haskell{let}-bindings transformed into src_haskell{(>>=)}-bindings),
which gives the following definition of the corresponding analogue for src_haskell{mapa}
#+BEGIN_SRC haskell :tangle TngAleMain.hs
mapaE :: (r -> Either e (x -> y, (a, b)))
-> (a -> Either e x)
-> (r -> Either e (y, b))
mapaE = homWrap $ \st f -> chopE st $ \s a -> pure s <*> f a
#+END_SRC
\noindent (again, note that src_haskell{mapaE} is exactly src_haskell{mapa} with body lifted to src_haskell{Applicative}),
which can be encoded using the generalized encoding of of \cref{sec:ale:encoding} as
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs
newtype MapperE e r f a = MapperE { runMapperE :: r -> Either e (f, a) }
instance ApplicativeLike (MapperE e r (x -> y)) where
type C (MapperE e r (x -> y)) a b = (a, b)
type G (MapperE e r (x -> y)) a = a -> Either e x
type F (MapperE e r (x -> y)) b = MapperE e r y b
f <**> g = MapperE $ mapaE (runMapperE f) g
mapDeviceGE :: MapperE String Device Device ()
mapDeviceGE = MapperE (Right . depureMap Device unDeviceLISP)
<**> (\x -> if x then pure x else throwE' "bad")
<**> (\x -> pure (x + 100))
<**> (\x -> pure (x + 200))
testMapDeviceGE :: Either String Device
testMapDeviceGE = fmap runMap $ runMapperE mapDeviceGE exampleDevice
#+END_SRC
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs :exports none
throwE' = Left
#+END_SRC
Moreover, note that the above body of src_haskell{chopE} does not mention anything specific to src_haskell{Either}, thus it can be reused for all instances described in \cref{sec:instances:more} without modifications.
The following shows that the same property also holds for Scott-encoded data types.
Similarly to \cref{sec:scott} where we had to src_haskell{cons} to the left to get multiple stacks, in this case we also need to push the src_haskell{Either} (or another instance from \cref{sec:instances:more}) to the leftmost position
#+BEGIN_SRC haskell :tangle TngAleMain.hs
chopES :: ((Either e s -> a -> b) -> c)
-> (s -> a -> Either e t)
-> ((Either e t -> b) -> c)
chopES i f o = i $ \s a -> o (s >>= \s' -> f s' a)
mapaES :: (r -> (Either e (x -> y) -> a -> b) -> c)
-> (a -> Either e x)
-> (r -> (Either e y -> b) -> c)
mapaES = homWrap $ \st f -> chopES st $ \s a -> pure s <*> f a
#+END_SRC
\noindent Now, note that Scott-encoding allows not only simple src_haskell{cons}ing but it also allows one to apply a function to the element in the head
#+BEGIN_SRC haskell :tangle TngAleMain.hs
consApp :: (s -> t)
-> ((s -> a) -> b)
-> (t -> a) -> b
consApp st sab ta = sab $ \s -> ta (st s)
#+END_SRC
\noindent which allows to straightforwardly translate the other examples
#+BEGIN_SRC haskell :tangle TngAleMainGeneric.hs
newtype MapperES c e r f a = MapperES
{ runMapperES :: r -> (Either e f -> a) -> c }
instance ApplicativeLike (MapperES c e r (x -> y)) where
type C (MapperES c e r (x -> y)) a b = a -> b
type G (MapperES c e r (x -> y)) a = a -> Either e x
type F (MapperES c e r (x -> y)) b = MapperES c e r y b
f <**> g = MapperES $ mapaES (runMapperES f) g
mapDeviceGES :: MapperES c String Device Device c
mapDeviceGES = MapperES (consApp Right . depureMapS Device unDeviceScott)
<**> (\x -> if x then pure x else throwE' "bad")
<**> (\x -> pure (x + 100))
<**> (\x -> pure (x + 200))
testMapDeviceGES :: Either String Device
testMapDeviceGES = runMapS $ runMapperES mapDeviceGES exampleDevice
-- and similarly for zip
#+END_SRC
Of course, in practice, for Scott-encoded case one is likely to use Scott-encoded version of src_haskell{Either} instead of the plain one, but the term of src_haskell{chopES} above shows that it is of no consequence: as with src_haskell{chopE}, src_haskell{chopES} does not mention src_haskell{Either}, thus that term can be reused for other instances of \cref{sec:instances:more} by changing the type.
#+BEGIN_theorem
Therefore, all of the src_haskell{ApplicativeLike} structures described in this part can be extended with another index signifying errors in such a way that the resulting structures become Cartesian products of src_haskell{Monad} and src_haskell{ApplicativeLike}, with all the benefits described in \cref{sec:products}.
#+END_theorem
#+BEGIN_proof
By the above reasoning.
#+END_proof
** Discussion
@@tex:\label{sec:ale:discussion}@@
From a practical perspective, in this part we have shown that by implementing a series of rather trivial state transformers we called src_haskell{chop*} and wrappers into a src_haskell{(->) r} src_haskell{Reader} we called src_haskell{homWrap*} and then composing them one can express operators that can express arbitrary computations for generalized multi-stack machines using a rather curious form of expressions very similar to conventional src_haskell{Applicative} parsers.
Then, we demonstrated how to use those operators to implement src_haskell{Applicative}-like pretty-printers, src_haskell{map}s, and src_haskell{zip}s between simple data types of a single constructor by first unfolding them into LISP- and Scott-encoded representations and then folding them back with custom "step-by-step" src_haskell{fold}s.
(Where the very fact that Scott-encoded case is even possible is rather fascinating as those terms are constructed using a rather unorthodox technique.)
#+BEGIN_remark
By the way, note that Haskell's src_haskell{GHC.Generics}~\cite{GHC86:base412:Generics} is not an adequate replacement for LISP- and Scott-encoded representations used in the document: not only is the src_haskell{Rep} type family complex, its structure is not even deterministic as GHC tries to keep the resulting type representation tree balanced.
Which, practically speaking, suggests another GHC extension.
#+END_remark
From a theoretical perspective, in this part we have presented a natural generalization of the conventional src_haskell{Applicative}~\cite{mcbride-paterson-08} type class (which can be viewed as a generalization of conventional function application) into dependent types with generalized arrow of src_haskell{Category}/src_haskell{ArrowApply}~\cite{Hackage:base4900, hughes-arrows-00}.
Both src_haskell{Applicative}s and src_haskell{Monad}s~\cite{moggi-89, moggi-91, Wadler:1992:EFP} (that can be viewed as a generalization of the conventional sequential composition of actions, aka "imperative semicolon") were similarly generalized to superapplicatives and supermonads in~\cite{Bracker2018:SS}.
In particular, \cite{Bracker2018:SS} starts by giving the following definition for src_haskell{Applicative}
#+BEGIN_SRC haskell-spec
class Applicative m n p where
(<*>) :: m (a -> b) -> n a -> p b
#+END_SRC
\noindent then adds constraints on top to make the type inference work, and then requires all of src_haskell{m}, src_haskell{n}, and src_haskell{p} to be src_haskell{Functor}s (producing such a long and scary type class signature as the result so that we decided against including it here).
In contrast, our src_haskell{ApplicativeLike} generalizes the arrow under src_haskell{m}, goes straight to dependent types for src_haskell{n} and src_haskell{p} instead of ad-hoc constraints, and doesn't constrain them in any other way.
#+BEGIN_remark
Which suggests syntactic (rather than algebraic) treatment of src_haskell{ApplicativeLike} structure as it seems that there are no new interesting laws about it except for those that are true for the conventional function application (e.g., congruence src_haskell{a == b => f a == f b}).
#+END_remark
In other words, our src_haskell{ApplicativeLike} can be viewed as a simpler encoding for generalized superapplicatives of~\cite{Bracker2018:SS} when those are treated syntactically rather than algebraically (since we completely ignore src_haskell{Functor}s).
* Transforming Trees with Indexed src_haskell{Monad}s
@@tex:\label{sec:pim}@@
#+BEGIN_SRC haskell :tangle TngIxState.hs :exports none
{-# LANGUAGE RebindableSyntax #-}
import Prelude (undefined, (.), ($), id, const, head, map, concat, concatMap, fst, snd, Bool(..), Char(..), String, (++), Int, Show(..), Num(..), Eq(..), (&&))
import Data.Either
import Data.List.Utils (uniq)
-- 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
** Motivation
Conventional src_haskell{Monad}ic parser combinators, as noted in~\cref{sec:parser-combinators}, allow us to express arbitrary transformations from src_haskell{Stream}s to arbitrary data types.
Conventional src_haskell{Applicative} parsers, as noted in~\cref{sec:ale:motivation}, allow us to very conveniently express simple transformations from src_haskell{Stream}s to simple data types of a single constructor.
src_haskell{ApplicativeLike} structures, which are dependently typed generalizations of src_haskell{Applicative}s, introduced in~\cref{sec:ale} allow us to very conveniently express simple transformations from simple data types of a single constructor to src_haskell{Stream}s, simple src_haskell{fold}s between such data types, and, as noted in~\cref{sec:general-case}, somewhat less conveniently, arbitrary transformations between such data types.
Clearly, a generalization of src_haskell{Monad}ic parser combinators that would allow us to express arbitrary transformations between arbitrary data types would nicely complete the picture.
In this part we shall describe such a generalization.
\Cref{sec:pim:motivating-examples} provides some motivating examples.
\Cref{sec:pim:derivation} derives said generalizations of src_haskell{Monad}ic parser combinators.
\Cref{sec:pim:examples} provides example usages, including the implementation of the motivating examples.
\Cref{sec:pim:discussion} discusses the consequences and the general picture.
*** Motivating Examples
@@tex:\label{sec:pim:motivating-examples}@@
Consider the following data type encoding for XML documents
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
data XML = Plain String
| Node String [(String, String)] [XML]
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
deriving instance Show XML
#+END_SRC
\noindent where src_haskell{Plain} represents inner plain text data and src_haskell{Node} represents an XML node with its parameters and children nodes.
For instance,
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
exampleXHTML :: XML
exampleXHTML =
Node "html" [("lang", "en")]
[ Node "body" []
[ Node "h1" [] [Plain "main title"]
, Node "div" [("class", "content")] $
[ Node "h2" [] [Plain "internal header"]
, Node "p" [] [Plain "some text"]
, Node "h2" [] [Plain "another internal header"]
, Node "p" [] [Plain "more text"]
]
]
]
#+END_SRC
Alternatively, consider the following representation of the same thing
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
data XMLElement = InnerText String
| StartTag String [(String, String)]
| EndTag String
type XMLStream = [XMLElement]
exampleXHTMLStream :: XMLStream
exampleXHTMLStream =
[ StartTag "html" [("lang", "en")]
, StartTag "body" []
, StartTag "h1" []
, InnerText "main title"
, EndTag "h1"
, StartTag "div" [("class", "content")]
, StartTag "h2" []
, InnerText "internal header"
, EndTag "h2"
, StartTag "p" []
, InnerText "some text"
, EndTag "p"
, StartTag "h2" []
, InnerText "another internal header"
, EndTag "h2"
, StartTag "p" []
, InnerText "more text"
, EndTag "p"
, EndTag "div"
, EndTag "html"
]
#+END_SRC
One probably would not be surprised to find either data type and a deserializer/serializer from/to either representation in a library for handling XML-encoded data.
Now, consider, for instance, the following problem: given a src_haskell{String} that contains a serialized XML document and a library that can parse such src_haskell{String}s into either of the above representations, produce a list of inner texts of =h2= headers containing a single plain text node inside.
How does one go about archiving that?
Conventionally, one either
- parses a given src_haskell{String} into an element of src_haskell{XML} type using the library, thus offloading all the "incorrectly formatted input" type of problems to the library, and then processes the result by inventing a specialized function that does a lot of src_haskell{concatMap}; or
- parses a given src_haskell{String} into src_haskell{XMLStream} using the library, and then treats the result as an input to a conventional parser built with the help of some parser combinator library, which allows one to easily and generically extract inner texts following src_haskell{StartTag "h2"} elements, but requires duplication of all the error handling for "incorrectly formatted input" type of problems the library already has; or
- parses into src_haskell{XML}, with usual benefits, and then accumulates results with some generalized traversal and pattern matching mechanism.
The issue becomes even more apparent when one has a tree structure which one can not simply src_haskell{traverse} (src_haskell{Traversable}~\cite{Hackage:base4900}) to collect some results.
Say, for instance, one needs to parse a src_haskell{String} representing a program into its abstract syntax tree (AST) and then apply some carefully crafted type-respecting rewrite rules to perform some program optimizations.
Assuming one wants to be able to change the type of AST without rewriting everything, one is now conventionally required to use something like SYB~\cite{Laemmel:2003:SYB}, Uniplate~\cite{Mitchell:2007:Uniplate}, Multiplate~\cite{Hackage:multiplate003}, or Lenses~\cite{Kmett:Lens, Hackage:lens417}, possibly combined with some generalized patter-matching machinery similar to~\cite{Rhiger:2009:TSP}.
Which is not to say that doing any of the above is inherently bad, but when a compiler you wrote parses its inputs into ASTs with src_haskell{Monad}ic and/or src_haskell{Applicative} parser combinators and emits results with some src_haskell{ApplicativeLike} machinery, all of which are just fancy state transformers, one starts to wonder whether the same "hammer" can be used for the term rewriting "nails" in the middle too.
** Derivation (and Cartesian Products)
@@tex:\label{sec:pim:derivation}@@
The logic behind the design of a generalized structure that can express arbitrary tree transformers src_haskell{Monad}ically is rather straightforward.
We know that conventional src_haskell{Monad}ic parser combinators like Parsec, Attoparsec, and Megaparsec are made of amalgamations of src_haskell{State}
#+BEGIN_SRC haskell-spec
newtype State s a = State { runState :: s -> (a, s) }
#+END_SRC
\noindent with src_haskell{Either} (then, usually, Scott-encoded).
Therefore, since we now want state transformers that work over arbitrary trees instead of just src_haskell{Stream}s, and in~\cref{sec:deriving-the-technique} we saw that all we needed to archive the same result there was to decouple two type variable entries of src_haskell{s}, all we have to do now is to perform the same modification to src_haskell{State}, thus archiving the exact definition of src_haskell{IxState} from~\cref{sec:not-tutorial:indexed-state}
#+BEGIN_SRC haskell-spec
data IxState i j a = IxState { runIxState :: i -> (a, j) }
#+END_SRC
\noindent Finally, since here we, too, need to handle errors, we need to amalgamate src_haskell{Either} into it.
As before, there are several possibilities here which we shall discuss in the following sections.
Before that, however, note that we are now essentially discussing translations of conventional src_haskell{Monad}ic parser combinators of~\cref{sec:parser-combinators} which we generalized with src_haskell{Monad}ic error handling in~\cref{sec:instances:parser-combinators} into indexed src_haskell{Monad} (src_haskell{IxMonad}) territory discussed in~\cref{sec:not-tutorial:indexed-monads}.
*** Instance: Simple Indexed src_haskell{Monad}ic Parser Combinator
@@tex:\label{sec:pim:without-access}@@
Adaptation of src_haskell{SParser} parser combinator of~\cref{sec:parser-combinators:without-access} to the indexed src_haskell{IxMonad} case is straightforward, all the terms stay the same up to constructor and variable renames
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
newtype IxSParser e i j a = IxSParser
{ runIxSParser :: i -> Either e (a, j) }
instance IxPointed (IxSParser e) where
ipure a = IxSParser $ \i -> Right (a, i)
instance IxMonad (IxSParser e) where
p >>=+ f = IxSParser $ \i ->
case runIxSParser p i of
Left x -> Left x
Right (a, j) -> runIxSParser (f a) j
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
instance IxFunctor (IxSParser e) where
ifmap = iliftM
instance IxApplicative (IxSParser e) where
(<*+>) = iap
#+END_SRC
As with src_haskell{SParser}, src_haskell{IxSParser} has a single implementation for src_haskell{Monad} in index src_haskell{e} that form a plain src_haskell{Monad}.
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
throwIxSP :: e -> IxSParser e i j a
throwIxSP e = IxSParser $ \_ -> Left e
-- Note that this keeps indices as is, since it is a `Monad`,
-- not `IxMonad` in `e`
catchIxSP :: IxSParser e i j a -> (e -> IxSParser f i j a) -> IxSParser f i j a
catchIxSP m f = IxSParser $ \i ->
case runIxSParser m i of
Right x -> Right x
Left e -> runIxSParser (f e) i
#+END_SRC
Thus, to define an analogue of src_haskell{ConjoinedMonads} for src_haskell{IxSParser}, following the discussion in~\cref{sec:products}, we need to make a product of src_haskell{Monad} with src_haskell{IxMonad}.
Skipping all the Haskell encoding discussion of~\cref{sec:encodings} and~\cref{sec:products}, let us simply define this structure as
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
class MonadXIxMonad m where
icpure :: a -> m e i i a
icbind :: m e i j a -> (a -> m e j k b) -> m e i k b
icthrow :: e -> m e i j a
iccatch :: m e i j a -> (e -> m f i j a) -> m f i j a
-- `(>>)` in index `a`
iandThen :: MonadXIxMonad m => m e i j a -> m e j k b -> m e i k b
iandThen f g = f `icbind` const g
-- `(>>)` in index `e`
iorElse :: MonadXIxMonad m => m e i j a -> m f i j a -> m f i j a
iorElse f g = f `iccatch` const g
-- `ifmap` derived for MonadXIxMonad in index `a`, for later simplicity
ifmap' :: MonadXIxMonad m
=> (a -> b) -> m e i j a -> m e i j b
ifmap' f m = m `icbind` \a -> icpure (f a)
-- `iap` derived for MonadXIxMonad in index `a`, for later simplicity
iiap' :: MonadXIxMonad m
=> m e i j (a -> b) -> m e j k a -> m e i k b
iiap' mf m = mf `icbind` \f -> m `icbind` \a -> icpure (f a)
#+END_SRC
\noindent and its instance as
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
instance MonadXIxMonad IxSParser where
icpure = ipure
icbind = (>>=+)
icthrow = throwIxSP
iccatch = catchIxSP
#+END_SRC
#+BEGIN_theorem
src_haskell{IxSParser} is a src_haskell{Monad} in index src_haskell{e} and an src_haskell{IxMonad} in index src_haskell{a}.
Moreover, operators of those instances satisfy the interaction laws identical to those of \cref{dfn:proper}.
#+END_theorem
#+BEGIN_proof
By case analysis.
#+END_proof
Similarly to \cref{sec:instances:parser-combinators:interesting}, this structure also has type-precise src_haskell{some} and src_haskell{many} operators
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
icsome :: MonadXIxMonad m
=> m e i i a -> m e i i [a]
icsome p = ifmap' (:) p `iiap'` icmany p
icmany :: MonadXIxMonad m
=> m e i i a -> m f i i [a]
icmany p = icsome p `iorElse` icpure []
#+END_SRC
\noindent (However, unlike in \cref{sec:instances:parser-combinators:interesting} here we use derived src_haskell{iiap'} and src_haskell{ifmap'} combinators instead of using those of src_haskell{IxApplicative} thus simplifying the type class constraints.)
The most interesting thing about src_haskell{IxSParser} are the types of src_haskell{sepBy*} combinators
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
-- zero of more `p` separated by `sep`
isepBy :: MonadXIxMonad m => m e i i a -> m e i i b -> m f i i [a]
isepBy p sep = isepBy1 p sep `iorElse` icpure []
-- one or more `p` separated by `sep`, that is
-- `p` followed by zero or more `sep >> p`
isepBy1 :: MonadXIxMonad m
=> m e i j a -> m e j i b -> m e i j [a]
isepBy1 p sep = p `icbind` \x ->
icmany (sep `iandThen` p) `icbind` \xs ->
icpure (x:xs)
#+END_SRC
\noindent Note how in src_haskell{isepBy1} the parser given in the first argument (src_haskell{p}) transforms the internal state src_haskell{i -> j} while the one given in the second (src_haskell{sep}) does the reverse.
*** Non-instance: \dots with Full Access to the State
On the other hand, adapting src_haskell{EParser} to the indexed case is not so trivial.
Note that a naive adaptation gives two possibilities that use different indexes for the src_haskell{Left} case
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
newtype IxEParserR e i j a = IxEParserR
{ runIxEParserR :: i -> Either (e, i) (a, j) }
newtype IxEParserC e i j a = IxEParserC
{ runIxEParserC :: i -> Either (e, j) (a, j) }
#+END_SRC
However, for src_haskell{IxEParserR} the types force the potential implementation of src_haskell{(>>=+)} to rollback the internal state on failure in the second argument
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
instance IxPointed (IxEParserR e) where
ipure a = IxEParserR $ \i -> Right (a, i)
-- not really, violates laws
instance IxMonad (IxEParserR e) where
p >>=+ f = IxEParserR $ \i ->
case runIxEParserR p i of
Left x -> Left x
Right (a, j) -> case runIxEParserR (f a) j of
Left (e, _) -> Left (e, i)
Right x -> Right x
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
instance IxFunctor (IxEParserR e) where
ifmap = iliftM
instance IxApplicative (IxEParserR e) where
(<*+>) = iap
#+END_SRC
\noindent which violates the associativity law of src_haskell{Monad} (see \cref{sec:monad}), since, for instance
#+BEGIN_SRC haskell-spec
let
modify = IxEParserR $ \i -> Right ((), delta i)
f = modify
g = throw e
in
(f >>+ g) >>=+ h == throw e
-- but
f >>+ (g >>=+ h) == modify >>+ throw e
#+END_SRC
\noindent which are not equal when src_haskell{i /= delta i} for some src_haskell{i}.
Meanwhile, for src_haskell{IxEParserC} the src_haskell{(>>=+)} operator simply has no implementation.
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
instance IxPointed (IxEParserC e) where
ipure a = IxEParserC $ \i -> Right (a, i)
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
-- not really, undefined
instance IxMonad (IxEParserC e) where
p >>=+ f = IxEParserC $ \i ->
case runIxEParserC p i of
Left (e, j) -> undefined -- neither `Left (e, i)` nor `Left (e, j)`
Right (a, j) -> runIxEParserC (f a) j
#+END_SRC
#+BEGIN_SRC haskell :tangle TngEmeMain.hs :exports none
instance IxFunctor (IxEParserC e) where
ifmap = iliftM
instance IxApplicative (IxEParserC e) where
(<*+>) = iap
#+END_SRC
*** Instance: Twice Conjoinedly Indexed src_haskell{Monad}ic Parser Combinator with Full Access to the State
Interestingly, to make a working adaptation of src_haskell{EParser} to the indexed case we have to add another index to the data type signature to signify =state-after-error= (denoted as src_haskell{k} in the following signature)
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
newtype IxEParser e i k j a = IxEParser
{ runIxEParser :: i -> Either (e, k) (a, j) }
#+END_SRC
\noindent and then take a product of two src_haskell{IxMonad} instances for indexes src_haskell{i j} for the index src_haskell{a} (as before) and indexes src_haskell{i k} for the index src_haskell{e} (which is new, and weird)
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
class IxMonadXIxMonad m where
iicpure :: a -> m e i u i a
iicbind :: m e i u j a -> (a -> m e j u k b) -> m e i u k b
iicthrow :: e -> m e i i u a
iiccatch :: m e i j u a -> (e -> m f j k u a) -> m f i k u a
-- `(>>+)` in index `e`
iiorElse :: IxMonadXIxMonad m => m e i j u a -> m f j k u a -> m f i k u a
iiorElse f g = f `iiccatch` const g
iifmap :: IxMonadXIxMonad m
=> (a -> b) -> m e i u j a -> m e i u j b
iifmap f m = m `iicbind` \a -> iicpure (f a)
iiap :: IxMonadXIxMonad m
=> m e i u j (a -> b) -> m e j u k a -> m e i u k b
iiap mf m = mf `iicbind` \f -> m `iicbind` \a -> iicpure (f a)
#+END_SRC
Arguably, the resulting class signature becomes rather unreadable when encoded using the simplest encoding for GHC Haskell, thus let us also demonstrate how this class would be encoded using the imaginary idealized encoding of \cref{sec:encodings}.
#+BEGIN_SRC haskell-spec
class (forall j a . IxMonad (\i k e -> m e i k j a) -- `IxMonad` in `e`
, forall k e . IxMonad (\i j a -> m e i k j a)) -- `IxMonad` in `a`
=> IxMonadXIxMonad m where
#+END_SRC
#+BEGIN_theorem
src_haskell{IxEParser} is an src_haskell{IxMonad} in index src_haskell{e} and an src_haskell{IxMonad} in index src_haskell{a}.
Moreover, operators of those instances satisfy the interaction laws identical to those of \cref{dfn:proper}.
#+END_theorem
#+BEGIN_proof
By case analysis.
#+END_proof
Of especial note here is the fact that this time the two src_haskell{IxMonad}s of this product interact not only with the operational interaction laws of \cref{dfn:proper} like all other similar products but, in some sense, they also interact in types by "sharing" index src_haskell{i}.
Moreover, note that src_haskell{IxEParser}, unlike src_haskell{EParser}, admits only a single implementation of the src_haskell{iiccatch}
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
instance IxMonadXIxMonad IxEParser where
iicpure a = IxEParser $ \i -> Right (a, i)
iicbind p f = IxEParser $ \i ->
case runIxEParser p i of
Left x -> Left x
Right (a, j) -> runIxEParser (f a) j
iicthrow e = IxEParser $ \i -> Left (e, i)
-- analogous to `catchEPC`
iiccatch m f = IxEParser $ \i ->
case runIxEParser m i of
Right x -> Right x
Left (e, j) -> runIxEParser (f e) j
#+END_SRC
\noindent which continues with the latest state on error.
Meanwhile, the version that rolls-back has a different type:
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
-- analogous to `catchEPR`
catchIxEPR :: IxEParser e i u j a -> (e -> IxEParser f i k j a) -> IxEParser f i k j a
catchIxEPR m f = IxEParser $ \i ->
case runIxEParser m i of
Right x -> Right x
Left (e, j) -> runIxEParser (f e) i
#+END_SRC
As usual, the types of the corresponding src_haskell{some} and src_haskell{many} combinators are very informative.
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
iicsome :: IxMonadXIxMonad m => m e i k i a -> m e i k k [a]
iicsome p = iifmap (:) p `iiap` iicmany p
iicmany :: IxMonadXIxMonad m => m e i k i a -> m f i u k [a]
iicmany p = iicsome p `iiorElse` iicpure []
#+END_SRC
\noindent Arguably, a bit /too/ informative.
** Examples
@@tex:\label{sec:pim:examples}@@
For reasons discussed in \cref{sec:pim:discussion} we shall ignore src_haskell{IxEParser} and concentrate on examples that can be implemented with src_haskell{IxSParser}.
Firstly, as usual, if we so desire, we can have our own version of src_haskell{(<|>)} operator from src_haskell{Alternative} with error collection in a src_haskell{Monoid}
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
(<|+>) :: (MonadXIxMonad m, Monoid e)
=> m e i j a -> m e i j a -> m e i j a
f <|+> g = f `iccatch` \e ->
g `iccatch` \e' ->
icthrow (e `mappend` e')
-- A useful generalization
class Monoid e => Failure e where
-- expected `a` but got `b` instead
expected :: String -> String -> e
-- unexpected `a`
unexpected :: String -> e
instance Failure [String] where
expected a b = ["expected " ++ a ++ " got " ++ b]
unexpected a = ["unexpected " ++ a]
#+END_SRC
\noindent Then, of course, we can have both usual operators to manipulate the internal state, similarly to the conventional src_haskell{State} src_haskell{Monad}
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
iget :: IxSParser e i i i
iget = IxSParser $ \i -> Right (i, i)
iput :: j -> IxSParser e i j ()
iput j = IxSParser $ \_ -> Right ((), j)
#+END_SRC
\noindent Then, we can have all the usual src_haskell{Monad}ic parser combinators (including src_haskell{icsome}, src_haskell{icmany}, src_haskell{isepBy}, src_haskell{isepBy1} already discussed in \cref{sec:pim:without-access})
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
lookAhead :: IxSParser e i j a -> IxSParser f i i (Either e a)
lookAhead p = IxSParser $ \i -> case runIxSParser p i of
Left e -> Right (Left e, i)
Right (a, j) -> Right (Right a, i)
notFollowedBy :: (Failure e, Show a) => IxSParser f i j a -> IxSParser e i i ()
notFollowedBy p = lookAhead p >>=+ \ma -> case ma of
Left _ -> icpure ()
Right a -> icthrow $ unexpected $ show a
endOfInput :: (Failure e, Show i) => IxSParser e [i] () ()
endOfInput = IxSParser $ \i -> case i of
[] -> Right ((), ())
(i:_) -> Left $ expected "end of input" (show i)
anything :: Failure e => IxSParser e [i] [i] i
anything = IxSParser $ \i -> case i of
[] -> Left $ unexpected "end of input"
(i:is) -> Right (i, is)
-- etc
#+END_SRC
Now, to solve our motivational "inner text in h2 nodes" problem we just need a couple of generic combinators
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
exhaust :: IxSParser e i j a -> IxSParser e [i] () [a]
exhaust p = IxSParser $ \is -> Right (go is, ()) where
go [] = []
go (i:is) = case runIxSParser p i of
Left _ -> go is
Right (a, _) -> a:(go is)
find :: Failure e
=> IxSParser e i () a
-> IxSParser e i [i] b
-> IxSParser e i () [a]
find p w = (p >>=+ \a -> icpure [a])
`iccatch`
(\_ -> w >>=+ const (exhaust (find p w)) >>=+ \ps -> icpure (mconcat ps))
#+END_SRC
\noindent and a couple of trivial src_haskell{XML}-specific combinators
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
plain :: Failure e => IxSParser e XML () String
plain = IxSParser $ \i -> case i of
Plain s -> Right (s, ())
Node a _ _ -> Left $ expected "inner plain text node" ("`" ++ a ++ "' node")
node :: Failure e => IxSParser e XML [XML] String
node = IxSParser $ \i -> case i of
Node s _ w -> Right (s, w)
_ -> Left $ expected "node" "inner plain text"
#+END_SRC
\noindent which, taken together, allow us to write
#+BEGIN_SRC haskell :tangle TngEmeMain.hs
single :: (Failure e, Show i) => IxSParser e [i] i ()
single = anything >>=+ \a -> endOfInput >>=+ const (iput a)
childOf :: Failure e
=> IxSParser e XML () String -> String -> IxSParser e XML () String
childOf p n = node >>=+ \a -> if a == n
then single >>=+ const p
else icthrow $ expected n a
allPlainH2 :: IxSParser [String] XML () [String]
allPlainH2 = find (plain `childOf` "h2") node
testIxSParser = runIxSParser allPlainH2 exampleXHTML
== Right (["internal header","another internal header"],())
#+END_SRC
Moreover, note that the results of \cref{sec:ale} can also be adapted to this structure.
src_haskell{ApplicativeLike} structures describe generalized multi-stack machines, src_haskell{IxSParser} can similarly express them by hiding those "stacks" in its indexes.
In particular, note that src_haskell{chopE} of \cref{sec:ale:products} is, essentially, the src_haskell{(i -> j) -> IxSParser e i j a} that was turned on its head.
** Discussion
@@tex:\label{sec:pim:discussion}@@
From a practical perspective, in this part we have shown that src_haskell{Monad}ic parser combinators can be generalized to "parse" and transform between arbitrary data types.
From a theoretical perspective, we have demonstrated another couple of interesting Cartesian products (src_haskell{MonadXIxMonad} and src_haskell{IxMonadXIxMonad}) with their instances.
Note however, that while src_haskell{IxEParser} is an instance of a pinnacle of indexed src_haskell{Monad}ic structures discussed in this work, namely src_haskell{IxMonadXIxMonad}, and, clearly, that structure can be used to implement arbitrary transformations between data types, the author feels like from the parser combinator standpoint src_haskell{IxEParser} is an instance of "science has gone too far".
As discussed \cref{sec:parser-combinators:variants} (especially around footnote~\ref{fn:no-rollback}), in author's opinion, non-rolling-back parsers combinators are just too hard to reason with and src_haskell{IxEParser} does not give a choice in the matter of rollback semantics.
One can argue that the "I-have-to-wrap-everything-with-src_haskell{try}-combinator" problem of \cref{sec:parser-combinators:variants} can be solved by implementing a variant of src_haskell{(<|>)} operator of src_haskell{Alternative} that would do it automatically, but even then, the non-rolling-back src_haskell{catch} is similarly hard to reason with: for instance, in which state the src_haskell{b} of src_haskell{(a `catch` e) >> b} starts?
Nevertheless, src_haskell{IxMonadXIxMonad} is an interesting Cartesian product and the types of src_haskell{iicsome} and src_haskell{iicmany} operators of src_haskell{IxEParser} are very informative, regardless of their practicality.
Finally, note that while for purely src_haskell{Monad}ic parser combinators src_haskell{SParser} was, essentially, a special case of src_haskell{EParser} (see \cref{sec:instances:parser-combinators}), in the indexed src_haskell{Monad} case src_haskell{IxSParser} is not a special case of src_haskell{IxEParser} since src_haskell{catchIxEPR} is not an instance of src_haskell{iiccatch}.
* Conclusions and Future Work
:PROPERTIES:
:UNNUMBERED: true
:END:
@@tex:\label{sec:conclusions}@@
In short, in this work we have shown that natural generalizations of src_haskell{Applicative} and src_haskell{Monad} type classes of Haskell combined with the ability to make Cartesian products of them produce a very simple common framework for expressing many practically useful things which include src_haskell{throw/try/catch} exception handling and various computations expressing transformations between data types that rather loosely (but, in important respects, usefully) follow conventional src_haskell{Applicative} and src_haskell{Monad}ic programming idioms.
Thus, indexed generalizations of src_haskell{Applicative} and src_haskell{Monad}ic structures, most importantly, generalizations of src_haskell{State} and src_haskell{Either}, are rather powerful "hammers" that can handle a surprising number of different types of "nails".
In terms of related works this work contributes the following:
- \Cref{sec:eme}, essentially, extends the work of Wadler~\cite{Wadler:1992:EFP} by showing that src_haskell{Monad}s can also be used for proper error handling (and not just "hiding errors from the higher-level interpreter"), the observation which we formalized into src_haskell{ConjoinedMonads} structure in \cref{sec:encodings}.
Similarly to how Wadler's src_haskell{Monad} instances influenced the design of modern Haskell, instances discussed in \cref{sec:eme} also hint at new language design opportunities, which we discussed in \cref{sec:products,sec:eme:discussion}.
- \Cref{sec:ale} extends the work of McBride and Paterson~\cite{mcbride-paterson-08} on src_haskell{Applicative}s by showing other interesting structures that follow the same general form of expressions but allow for more sophisticated transformations, a structure which we formalized into the src_haskell{ApplicativeLike} type class in \cref{sec:ale:encoding} and discussed the consequences of in \cref{sec:ale:discussion}.
- \Cref{sec:pim}, essentially, extends works on parser combinators, most notably the work of Leijen and Meijer~\cite{Leijen:2001:PDS}, to "parsing" arbitrary data types.
Note, however, that most of those results are applicable outside of Haskell.
For instance, src_haskell{Monad}ic observations are applicable to all languages that can explicitly override a linear composition ("semicolon") operator.
Thus, for instance, they can be applied to practically any language by using a pre-processor, the language in question can be kept unaware of any src_haskell{Monad}ic structures.
Meanwhile, src_haskell{ApplicativeLike} observations can be applied to all languages with function calls.
The type system does not matter unless one wants to explicitly give types to those terms, which is not a strict requirement for applying the ideas discussed in this work.
Regarding specifically the Haskell language:
- src_haskell{ConjoinedMonads} of \cref{sec:eme} and other similar Cartesian products discussed throughout the work require language extensions and/or modifications to type class inference mechanisms of Haskell to make them usable (that is, to make the same functions available for reuse between "computation" and "error handling" contexts) in actual programs, as discussed \cref{sec:encodings},
- src_haskell{ApplicativeLike} type class can already be encoded in Haskell, though not in a particularly beautiful way, as discussed in \cref{sec:ale:encoding},
- a language extension or a set of Template Haskell functions the =base= library providing LISP- and/or Scott-encoded representations for given data types would make results presented in \cref{sec:ale} much more pleasant to use.
As a general observation, note that the space of composable state transformers, of which our src_haskell{ApplicativeLike} and src_haskell{IxMonad}ic structures are rather trivial examples, clearly contains a lot of structures that have their applicability to programming practice completely unexplored.
Most of this work, essentially, explores a single such structure (and its categorical dual), but it is fairly clear that there are other structures with similar properties (e.g., remember \cref{sec:instances:throw-catch-cc,sec:scott}).
Moreover, \cref{sec:pim} hints that there are likely to exist even more generic algebraic structures classifying those unexplored state transformers.
The author feels 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,
- application of the ideas of \cref{sec:ale} to the src_haskell{Alternative} type class to cover the multi-constructor case,[fn::
It is not entirely clear if this is possible, since it is not exactly clear how the canonical use of src_haskell{Alternative} for parsing tagged data types should look like in the first place, as, unlike the src_haskell{Applicative} case, different libraries use different idioms for this.]
- 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}.]