# 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 vice-versa: 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 Idris-specific. However, the syntax should hopefully not differ too much compared to other FP languages (e.g. Haskell).)

## Disclaimer

**This document is, by nature, a never-ending 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 function`putStrLn`

could be combined as`greeting >>= 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 side-effect (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

“first-class” — being able to use the concept everywhere in the language, e.g. functions are

*first-class*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`

and`snd`

to retrieve`a`

and`b`

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`

and`snd`

such that I can call`fst`

on it to get the thing’s first element and`snd`

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`

to`Nat`

” means “a function that takes an`Int`

and returns a`Nat`

”.

- 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.

“eta-expansion” ($\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, and`w`

(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).

- since Idris (and Haskell) may be considered a category, all functors in them
are technically
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 : )