Functional Programming Nomenclature Intro
Table of Contents
Preface
When starting out in functional programming (FP), you’ll likely see a lot of syntax in the languages that you have never come across before and therefore don’t know how to pronounce. Or viceversa: someone might keep referring to “the ‘bind’ operator” without you having a clue what that looks like in the language you’re working in. The aim of this post is to try to cover most of those things.
The motivation for creating this post was/is deeply personal. When I first started my Ph.D., I encountered a multitude of terms and concepts that everyone around me seemed to Just Know (TM), while I was left feeling perplexed and out of the loop. Eventually, through numerous awkward questions and conversations where I felt quite foolish, I managed to unravel the meanings of these arcane terms and symbols. Since, as far as I could tell, there wasn’t a simple nomenclature out there (“simple” meaning “answering ‘what is this called?’ without raising exponentially more questions”) I decided to put together this reference to hopefully help others avoid the same confusion and headaches I faced.
You can read it in one go and try to remember the terms, but I believe it might work better as a lookup reference that you have open adjacent to whatever you’re currently working on. But that’s up to you : )
In any case, the idea is that reading this should at least let you think about FP in words rather than mystical runes you don’t understand (which I’ve personally found can be difficult). It should also, hopefully, make it easier to talk about FP things or understand the feedback you get given from other FP people.
(Note: Since I mainly do functional programming in Idris, some of these examples will be Idrisspecific. However, the syntax should hopefully not differ too much compared to other FP languages (e.g. Haskell).)
Disclaimer
This document is, by nature, a neverending Work In Progress, and the explanations are only as good as my own understanding. Should you encounter any errors (or terms you would like added), please reach out on this website’s GitHub repository.
Syntax

>>=
— “bind”More details
Bind takes a result and a function which uses the result, and combines the two, e.g. a variable
greeting
containing the string"Hello World"
and the functionputStrLn
could be combined asgreeting >>= putStrLn
which would print the greeting to the terminal when run.

>>
— “seq”, short for “sequence”More details
In Idris land, this behaves similar to “bind”, except it only works with things that produce a sideeffect (e.g. printing to the terminal) without also returning a new value to handle.

:
— “has/of type” in Idris, and “cons” in Haskell (yes this is confusing) 
::
— “cons” in Idris, and “has/of type” in Haskell (yes this is confusing) 
[]
— also referred to as “Nil” 
()
— “unit”, sometimes also written as:Unit
Terms

“firstclass” — being able to use the concept everywhere in the language, e.g. functions are firstclass if you can manipulate them just like you would any other term in the language (assign them to variables, pass them to other functions, put them in data structures, etc).

“a record” — a data structure containing named fields of data where those names are automagically also turned into functions (getters).
Typically, records also come with special syntax to update their fields. 
“a projection” — a getter for a record (functional programmers like to use maths terminology).

“data” — things that you create by describing how to construct them, e.g.
MkPair a b
is a data constructor used to create a pair(a, b)
More on pairs
Pairs typically also have the projections (getter functions)
fst
andsnd
to retrievea
andb
respectively. 
“codata” — things that you create by defining their getters rather than their constructors; effectively describing how to deconstruct the thing. For example, we could define a ‘CoPair’ as “a thing that has the projections
fst
andsnd
such that I can callfst
on it to get the thing’s first element andsnd
to get the thing’s second element”. Why? Mainly because it allows us to define infinite things: a
Stream
is a thing you deconstruct by taking the first element, followed by a stream of potentially infinitely more things. As long as we can take at least one element, which is the projection (getter function), everything is fine and we can reason about it.
 Why? Mainly because it allows us to define infinite things: a

“mapping” — synonymous with “function”
 Usually found in combination with “from a to b”, e.g. “a mapping from
Int
toNat
” means “a function that takes anInt
and returns aNat
”.
 Usually found in combination with “from a to b”, e.g. “a mapping from

“pure” — something which does not produce any side effects (like printing to the terminal) and returns the same output given the same input

“covering” — a function where you have defined what to return for all its possible inputs.

“total” — in Idris: a function which is either covering or productive (what is considered total varies from language to language).

“partial” — a function where you have not defined what to do for every possible input, or a function which may never terminate. In opposition to “total”.

“bottom” (also written
__
or $\bot$) — something which is provably false or absurd. If you can “construct bottom”, you should have a contradiction somewhere. 
“top” (also written $\top$) — something which is trivially true; a tautology.

“etaexpansion” ($\eta$expansion) — TODO

“binders” — TODO
 “lambda binders” ($\lambda$binders) — TODO
 “Pi binders” ($\Pi$binders) — TODO

“rig” — in Idris: the accessibility, i.e.
0
for erased,1
for linear, andw
(the default, usually not written) for unrestricted.Show technical definition
A rig is a mathematical concept. It is a set of elements with two binary operations “add” and “multiply” such that both operations have an identity (e.g. 0 and 1 respectively for natural numbers), multiplication distributes over addition, both operations are commutative (a + b = b + a), and multiplying by the additive identity (0 for natural numbers) always returns that identity (so for natural numbers: a * 0 = 0 * a = 0).
The name “rig” comes from “ring without negation” (Get it? We remove the ’n' from “ring” to get “rig” because it doesn’t have Negation. Mathematicians truly are funny people…)
The accessibilities in Idris form a rig, hence we refer to them as such. 
“rig 0” — in Idris: erased / runtime inaccessible.

“rig 1” — in Idris: linear / must be used exactly once.

“rig w” — rig omega; in Idris: unlimited use.

$\cong$ — TODO

$\preceq$ — TODO

$\vdash$ — TODO
Category Theory terms
Category Theory (CT) is a whole area of maths, explaining it is beyond the scope of this blog entry. Unfortunately for us, a lot of FP is built on ideas and concepts from CT so we have to at least be aware of it and know some of the terminology…
Category Theory for Programmers
Bartosz Milewski has a blog series called “Category Theory for Programmers” (also available as a book), which covers the “basics” of CT. I have put ‘basics’ in quotes here, because I own the book and read the first section, about 120 dense pages, after which Bartosz concludes “We’ve learned the basic vocabulary of category theory.” At this point, I gave up.
To be clear, it is many times better than any of the more formal
literature at explaining these things! It just also, in my opinion, goes way
above and beyond what the everyday functional programmer will ever need, and the
explanations have on multiple occasions hurt my brain (I’m still not sure if I
actually understand contravariant functors or if my brain has tricked itself
into thinking it understands it to avoid further headaches…). The first
couple of entries/chapters might be worth a read, but beyond that you’re doing
it out of masochistic tendencies personal interest.

“category”
 don’t think “a category of what?”
 it’s a mathematical way of describing things which have a common structure
 examples: TODO
 “My understanding is that a category describes a whole category of systems or the theories that share the same structure.” – Bartosz Milewski

“functor” — a mapping from one category to another
 TODO: examples

“endofunctor” — a mapping from a category to itself
 since Idris (and Haskell) may be considered a category, all functors in them are technically endofunctors (and mathematicians like to be precise).

TODO: eventually get to the infamous “A monad is just a monoid in the category of endofunctors, what’s the problem?”
 actual quote:
“All told, a monad in X is just a monoid in the category of endofunctors of X, with product × replaced by composition of endofunctors and unit set by the identity endofunctor.” – Saunders Mac Lane, Categories for the Working Mathematician.
 actual quote:
Would You Like To Know More?

Blog series: Category Theory for Programmers

Book: The Little Typer
And as always, thanks for reading : )