How programming is mathematics, and perhaps more importantly; how mathematics is programming. Don’t take my word for it, see: Robert Harper.
Science offers the boldest metaphysics of the age. It is a thoroughly human construct, driven by the faith that if we dream, press to discover, explain, and dream again, thereby plunging repeatedly into new terrain, the world will somehow come clearer and we will grasp the true strangeness of the universe. And the strangeness will all prove to be connected, and make sense. – E. O. Wilson (1929-2021)
Everything I’ve seen so far and how it all makes sense.
It all started with a look at the representation of
computational effects in Haskell this led to the modelling of
partial functions f : A ⇀ B and thus to the Kleisli arrow
f : A → T(B) for some monad T and thence to the understanding of
monad as the thing that enables composition of Kleisli arrows.
See: A more formal view of Kleisli category
Is a way of making one mathematical object look like another, subject to a minimalistic principle that the “dressing” required to make the embedding work are such that the laws governing the desired structure are only those that are required by that structure and the “dressing” be as simple as possible (no baggage or superflous decoration). Nice.
A more formal defintion of this is to be found in the fundamental ideas of homomorphism and initial and terminal objects of Category theory.
This is the zoo of algebraic structures we may encounter, or whose properties/laws we may wish to leverage; with varying burdens of proof.
| Structure | Totality[1] | Associativity | Identity | Inverse | Commutativity |
|---|---|---|---|---|---|
| Semigroupoid | ✓ | ||||
| Small category | ✓ | ✓ | |||
| Groupoid | ✓ | ✓ | ✓ | ||
| Magma | ✓ | ||||
| Quasigroup | ✓ | ✓ | |||
| Unital magma | ✓ | ✓ | |||
| Semigroup | ✓ | ✓ | |||
| Loop | ✓ | ✓ | ✓ | ||
| Monoid | ✓ | ✓ | ✓ | ||
| Group | ✓ | ✓ | ✓ | ✓ | |
| Commutative monoid | ✓ | ✓ | ✓ | ✓ | |
| Abelian group | ✓ | ✓ | ✓ | ✓ | ✓ |
[1] Totality here is equivalent to the closure axiom.
A powerful technique of mathematics and programming is that of re-use; If we can show that our structure or object conforms to a well understood abstractions as above, we can inherit the relevant theorems and proofs with impunity. We may even get free as in beer along with free as in freedom!
See: Taming of effects in Haskell
Also see this presentation of the categorical perspective and a good way to think about monads:
Monads made difficult - Stephen Diehl
Also known as a tensor category for reasons that will be apparent.
See: Intro to the categorical approach
A monoid in a monoidal category has:
| object | M |
| unit | e : I -> M |
| multiplication | m : M ⊗ M -> M |
such that:
m ∘ (id_M ⊗ e) = u_l
m ∘ (e ⊗ id_M) = u_r
m ∘ (id_M ⊗ m) = m ∘ (m ⊗ id_M) ∘ α
Where:
u_l : M ⊗ I -> M and
u_r : I ⊗ M -> M
are the identity isomorphisms for the monoidal category, and
α : M ⊗ (M ⊗ M) -> (M ⊗ M) ⊗ M
is part of the associativity isomorphism of the category.
So, hopefully the connection is clear: we’ve generalized the carrier set to a carrier object, generalized the operations to morphisms in a category, and equational laws are promoted to being equations about composition of morphisms. – See: Haksell Wiki on Free Structure
A monad can be cast as a class of monoid objects. Given a category
| objects are endofunctors | F : C -> C |
| morphisms | natural transformations betwen functors |
| tensor product is composition | F ⊗ G = F ∘ G |
| identity is the identity functor | I |
Via specialisation to a monad we have:
| an endofunctor | M : C -> C |
| natural transformation | η : I -> M |
| natural transformation | μ : M ∘ M -> M |
So monad is a monoid in the category of endofunctors.
See also: The categorical perspective
There are two aspects to this construction:
- The ability to compose effectful computations via Kleisli arrows and
monadic actions.
See: Modelling effects
- To encode a program as a tree of computational actions restricted in effect by stronly typed co-products.
Some stuff on arrows/applicatives hidden in here
Some eDSL stuff hideen in here
- See nLab on trinitarianism
- Short video John Baez on symmetric monoidial categories
- Bob Harper, Steve Awodey et.al. (OPLSS 2012-)
Proposed as a new foundations for mathematics. Homotopy Type Theory (HoTT) represents the primary trinitarian research direction; seeking to unify ideas from Intuitionistic (Per-Martin Löf) type theory, algebraic topology and higher categories.
A : Type
| Proof theoretically | A is a proposition |
| Type theoretically | A is a construction or program |
| Geometrically or categorically | A is a space |
I have been learning Agda and there’s a whole bunch of (Per-Martin Löf) type theory and intuitionistic logic to report on. Watch this space.
- Programming languages foundations in Agda
- Cubical Agda and HoTT
- The HoTT Game
- Univalent foundations in Agda