MathHaskell Rosetta Stone  Part 1
This post begins a short series meant to serve as an informal guide to reading Haskell code and translating back and forth with mathematics. It’s meant to help members of r/CategoryTheory understand posts that use Haskell code to convey ideas. My hope is that this series should also find use among Haskell programmers, as exposure to some of the basic methods and terminology used in modern math.
 Part 1 (this post)
 Part 2 (pending)
 Type variables
 Type classes
 Constructor classes
 Part 3 (pending)
 Kinds
 Typelevel programming
Basic types and functions
Math is concerned with defining sets and functions. Analogously, Haskell code is concerned with defining types and functions.
The above code roughly translate to the following definitions:
 A set \(\mathrm{RealVec2}\),
 A singlevariable function \(\mathrm{rv2Norm}\),
 A twovariable function \(\mathrm{rv2Scale}\),
 A twovariable function \(\mathrm{rv2Add}\), and
 A twovariable function \(\mathrm{RV2}\).
Straightforward enough (except maybe for the \(\mathrm{RV2}\) bit). Let’s dig into the syntax of the Haskell code to understand each part.
Pattern matching and variables
The tag RV2
does a number of things.
 It ensures that the type
RealVec2
has no members in common with any other type (this is one reason why it’s called a tag).  It acts as a function that allows the programer to create data objects of type
RealVec2
. This is why it’s called a data constructor, and we useRV2
in this capacity in the formulae ofrv2Scale
andrv2Add
.  Third, notice that
RV2
is an injective function, allowing us to useRV2
to refer to arbitrary members ofRealVec2
. This is the main sense in whichRV2
is a tag: every member ofRealVec2
has a unique formRV2 x y
for some particularx
andy
inRealNumber
. We take advantage of this fact in the definitions ofrv2Norm
,rv2Scale
, andrv2Add
.
Expressing a data object in terms of a data constructor is called pattern matching.
Pattern matching is ubiquitous in Haskell.
To define rv2Norm
, we match its argument against the pattern that the RV2
data constructor follows: namely, the symbol RV2
followed by two variables representing the data objects contained in the fields of RV2
.
We do likewise in the definitions of rv2Scale
and rv2Add
.
Again, the names we choose for variables are arbitrary.
Before we move on, I should take a moment to be clear about what I mean by the word variable in this context. You might already know that programmers often use the word variable to refer to a region of program memory that can be referenced, read from, and written to by the program at various times during execution. That is not what I mean by variable in this sense. In this post, I use variable to mean an abstract symbol used as a placeholder for a functions eventual argument, that is, the usual meaning of the word, as it’s used in math.
A note on multivariable functions
Next, it’s time to have a little talk about the number of variables a Haskell function has.
When reading type signatures, the rightmost function arrow (the >
) takes precedence.
The above code would be equivalent to the following (valid) code.
Earlier, I conceived of the math counterpart to rv2Scale
as mapping \(\mathbb{R} \times \mathrm{RealVec2}\) to \(\mathrm{RealVec2}\).
Were I to maintain fuller fidelity to the meaning of the Haskell code, though, I would have used the following instead.
A Haskell function may take one, and only one, argument. When we speak of a multivariable function in Haskell, we really mean a function of one variable that returns a function. This might seem odd at first, but please consider that Haskell actually agrees with our notion of function arguments in math. When we speak colloquially of a twovariable (math) function, what we truly speak of is a function of a single variable—the domain merely happens to be a cartesian product.
\[\mathrm{rv2Scale} : \underbrace{\mathbb{R} \times \mathrm{RealVec2}}_{\text{this is still just one set!}} \to \mathrm{RealVec2} \\ \mathrm{rv2Scale} \underbrace{\big( r, (\mathrm{RV2}, x, y) \big)}_{\text{this is still just one argument!}} = ( \mathrm{RV2}, rx, ry )\]As it is in math, so it is in Haskell: all functions are singlevariable functions.
But still, instead of returning a function, I could have defined rv2Scale
as taking a pair as argument.
Haskell has builtin syntax for ordered pairs, even.
The type (RealNumber, RealVec2)
is the Haskell analog of the set \(\mathbb{R} \times \mathrm{RealVec2}\).
We could have used that to define rv2Scale
.
The reason haskellers favor using the formulation RealNumber > (RealVec2 > RealVec2)
(which is call the curried form) over the equivalent formulation (RealNumber, RealVec2) > RealVec2
(which is call the uncurried form) is simply due to Haskell’s syntax.
You must have noticed by now that Haskell’s syntax rules allow you to omit the parentheses normally used to indicate function application.
Function application parentheses may be omitted whenever the argument consists of a single symbol.
Because Haskell allows you to omit functionapplication parentheses, the curried formulation ends up being far more convenient to use and (arguably) easier to read than the uncurried formulation. There isn’t a deeper reason than that.
In summary, the code we’ve seen so far defines:
 a type,
RealVec2
;  a function
RV2
, with domain typeRealNumber
and codomain typeRealNumber > RealVec2
;  a function
rv2Norm
, with domain typeRealVec2
and codomain typeRealNumber
;  a function
rv2Scale
, with domain typeRealNumber
and codomain typeRealVec2 > RealVec2
;  a function
rv2Add
with domain typeRealVec2
and codomain typeRealVec2 > RealVec2
; and  a function
rv2Reflect
with domain typeRealVec2
and codomain typeRealVec2
.
Since their codomains are function types, rv2Scale
, rv2Add
, and RV2
all yield functions.
Even though it’s a little bit of a lie, it’s often convenient to think of such functionyieldingfunctions as having multiple variables.
 Think of
rv2Scale
as having two inputs, with typesRealNumber
andRealVec2
, and an output of typeRealVec2
.  Think of
rv2Add
as having two inputs, both with typeRealVec2
, and an output of typeRealVec2
.  Think of
RV2
as having two inputs, both with typeRealNumber
, and an output of typeRealVec2
.RV2
is injective when thought of this way, a fact we use when we pattern match.
Readers may choose to skip this next aside, unless they feel like really nerding out.
Simple sum types and branching
Haskell ships with a standard library called base.
base comes with several useful data types predefined.
Among them are Bool
and Ordering
.
In math, they would look something like this.
\[\mathrm{Bool} = \{ \mathrm{False}, \mathrm{True} \} \\ \mathrm{Ordering} = \{ \mathrm{LT}, \mathrm{EQ}, \mathrm{GT} \}\]Each of False
, True
, LT
, EQ
, and GT
is a data constructor with no fields.
Conceptually they are constants, uniquely identified and referenced by their respective names.
Branching logic
The base library defines various operations on these data types, such as the familiar boolean operations.
Here we see our first examples of branching logic in a Haskell function. Fundamentally, all branching in Haskell is done by pattern matching.

The branching in
not
and()
is accomplished by defining several different equations. Each such equation matches a different pattern of the arguments, in other words, a different combination of data constructors. 
(&&)
branches using acase
expression. Each case of thecase
expression matches a different pattern.
I could have defined (&&)
with multiple equations, like ()
, but I wanted to have an example that used a case expression.
We also see our first example of operators.
By giving them symbolic names, Haskell knows that we intend the functions (&&)
and ()
to be binary operators.
This is reflected in the equations defining these functions.
Final note on these before moving on, each of (&&)
and ()
really just needs two cases.
In fact, defining these functions this way may cause the program to do more computations than necessary.
Accordingly, Haskell syntax allows us to use an underscore (the character _
) to indicate a matchanything pattern.
Ifthenelse and guards
base provides a type Double
that implements IEEE 754 doubleprecision floating point arithmetic.
Let’s define a function that compares Double
s and yields an Ordering
.
x < y
is a member of Bool
, which we then pattern match.
Pattern matching a member of Bool
is such common idiom that Haskell has a syntactic shortcut for it.
We can style that in various different ways, to our preference.
All of those are still a bit clunky, so Haskell syntax has a shorthand for checking a series of conditions. The syntax is reminiscent of defining a piecewise function.
The translation to math is straightforward.
\[\mathrm{compareDoubles} : \mathrm{Double} \times \mathrm{Double} \to \mathrm{Ordering} \\ \mathrm{compareDoubles}(x, y) = \begin{cases} \mathrm{LT} & \text{if $x < y$} \\ \mathrm{GT} & \text{if $x > y$} \\ \mathrm{EQ} & \text{otherwise} \end{cases}\]Algebraic data types
Recall the types we’ve seen so far.
RealVec2
builds a type by packaging data objects from several other types into a single conceptual unit.
Virtually all programming languages have this feature, known under various different names.
Some call such types structs, some languages call them objects, other languages call them records, and so on.
Bool
and Ordering
are defined by enumerating their members.
Many programming languages support defining enumeration types, or enums, similarly.
In Haskell lingo, RealVec2
is an example of a product type.
Bool
and Ordering
as special cases of sum types, though we will see sum types that are much more general.
We will now see that the terminology, “product” and “sum,” is deserved.
Product types and universal projection maps
If you’re very clever, you may already have recognize RealVec2
as a categorical product of RealNumber
with itself.
We need to define the universal projection maps and verify the universal product property to make sure we’re right.
So, Haskell admits pairwise products of types.
In fact, Haskell can express the product of any number of types (up to machine limitations).
If A1
, A2
, …, AN
are types, we define their product as so.
The names P
, PCons
, p1
, p2
, …, pN
are arbitrary.
The ...
is pseudocode for however many types you have/underscores you need.
Defining the functions p1
, p2
, …, pN
can be rather tedious.
Haskell gives us a shorthand way to define both the product type and the projection maps at once, using named fields.
This has all the effects of the first code block.
It creates the function p1
, p2
, …, pN
and the function PCons :: A1 > A2 > ... > AN > P
.
It also has the additional effect that we may choose to supply arguments to PCons
either positionally or by name, to our preference.
Here’s what I mean.
When supplying arguments by name, we don’t need to remember the order in which the various fields were originally declared. Any permutation of the fields is valid. The below example is perfectly valid.
I slipped in a new concept there that Haskellers like to call “name punning.” I used “Person” as the name of the type and as the name of the data constructor. This is legal and valid haskell, and it’s pretty common, especially when a data type has only one data constructor.
Sum types and universal inclusion maps
Bool
and Ordering
are each defined by explicitly listing their members.
Most languages support this, and it’s typically called enumerated types, or enums.
In Haskell, a types that have more than one data constructor are called sum types.
One of Haskell’s innovative features is that it allows you to freely combine both product type and sum types.
Here we have a data type with three data constructors. The novel feature of Haskell is that it allows a programmer to give different fields to each constructor in an enumeration. (I know, it’s crazy that this is a novel feature in programming languages!)
Notice that the constructors Cash
and Complimentary
have the same fields.
Because of their tags, they will create different copies of Dollar
in Payment
.
Thus, we have defined a tagged union.
Tagged unions are coproducts of sets. Similarly, sum types in Haskell are coproducts of types.
A programming language supports definition of product type and coproduct types, it is said to support algebraic data types.
Closing
In this post, we say how arbitrary products and coproducts of Haskell types can be expressed as Haskell types. Roughly, we have a category similar to \(\mathrm{SET}\), where Haskell types are the objects and Haskell functions are the maps. That’s moreorless the case, although there are a few caveats that we might have time for at the end. In the mean time, it’s useful to limit our discussion to the fragment of Haskell were it is true. This observation, though, is far from the total extant to which Category theory bares its teeth in Haskell.
As a parting note, notice that in the proofs of claims 1 and 2, we defined the induced map in a very ad hoc, manual way. In the next post, we’ll see how to write a Haskell program that generates these induced maps, naturally. Moreover, slipping the word naturally in there was intentional. We will rely on a concept called type variables. With type variables, we will be able to turn the machinery of Haskell in on itself. Type variables will allow us to embed—and leverage, to great utility—functors and natural transformation within Haskell programs.