Algebraic Data-types are amongst those few gems in programming, which when we get used-to, it seems hard to imagine how we worked without them at all, all this time? They enable one of the killer features of functional programming & Haskell - Pattern-matching -. When i have to work in a language without ADTs (Algebraic Data-types), i sorely miss them.

Their fancy sounding name isn’t just for show either, there’s real “Algebra” in Algebraic Data-types.

In this post, we’ll explore the algebra behind them.

First, we’d need to get familiar with a few relevant fundamental concepts.

Cardinality

Before we can move to the actual algebra, we’d need to get familiar with the concept of Cardinality of types.

A type (in Haskell’s context) can roughly be understood as collection of values which are similar in some way. The Int type is a collection of all Integer values. A String type is a collection of all string values and so on.

The cardinality of a type is a property of that type which, represents the number of inhabitants of that type, or more simply put, the number of values in that type.

A quick demonstration:

Consider the familiar Bool Haskell type.

data Void -- it has NO values

data () = () -- it has 1 Value

data Bool = True | False -- it has 2 values

The cardinality of the Bool type is the number of values that inhabit it. We can see that it has only 2 values, the two type constructors.

That makes the cardinality of the Bool type, two. More formally, we represent it as

\[\begin{align*} \text{|Bool|} &= 2 &\text{similarly} \\ \text{|()|} &= 1 &\text{and} \\ \text{|Void|} &= 0 \end{align*}\]

The most important thing understanding the concept of cardinalities of types enables us to learn is that -

Any two types with the same cardinality will alway be isomorphic to one another

That little statement above has profound effects.

Which brings us to the second fundamental concept we’d need to know a little about, isomorphism.

Isomorphisms

An Isomorphism is a rather abstract concept, but we don’t need to go there. For our utilitarian understanding it suffices to simply define it as:- There is said to be an isomorphism between types n and m, such that there exist a set of functions to and from, such that:

to :: n -> m

from :: m -> n

such that composing any of those, one after another, should get you back to where you started.

to . from = id
-- and
from . to = id

So, if two types have the same cardinality, i.e. they have the same number of values inhabitanting them, then any 1-to-1 mapping between their elements can serve as these to and from functions. Does this one-to-one mapping needs to have an order or satisfy some deep and profound mathematical property? Well, None!

It may be any arbitarty mapping, any 1-to-1 mapping is just as good as any other, there are no correct or incorrect mapping here, given it’s a one-to-one mapping, it’s game.

Generally speaking, between two types of equivalent cardinality “n”, we can find n! unique isomorphisms. For our purposes, any of those isomorphims is fine, what’s more important is knowing that an isomorphism exists between the types.

An Isomorphism between the types n and m states that n and m, for all intents and purposes, are the same thing.

Sum, Product and Exponential types

If you’ve been working with Haskell for any amount of time, you’ve probably heard of phrases like “That’s a Sum type” or perhaps “a product type”, and wondered “why the odd names? i’m not summing or product-ing (that’s a real word) any types?”.

Well, you are, in terms of their cardinalities.

A sum type, as you might have guessed, probably corresponds to some sort of addition. A product type on the other hand might deal with some kind of multiplaction right? on-point guesses!

Sum types correspond to Addition (+)

The types whose cardinalities are a sum of their constituent types. They correspond to logical “ORs”. They usually have multiple data-constructors. A value of a sum-type is either this OR that, it cannot be both. For eg.

The cardinality of the type is the sum of cardinalities of it’s constructors.

data Either a b = Left a | Right b

-- |Either a b| = |a| + |b|


data Maybe a = Nothing | Just a

-- |Maybe a| = |Nothing| + |a|
--           = 1 + |a|

The above example illustrates how we sum-up the cardinalities of sum types, by adding the cardinalities of it’s constructors (which may further be sum/product types that need to be reduced).

The only surprising thing above is probably - why the cardinality of Nothing is 1? - Well, since there is only 1 Nothing ! (it is no different in that sense from when we saw the Bool example, where True had a cardinality of 1 and False had 1, while the total cardinality of Bool was 1 + 1 = 2)

Product types correspond to Multiplication (x)

While a sum type is analogous a logical “OR”, you may think that a product type is analogous to a logical “AND”.

a product type will have both a AND b values if it’s a product of those two.

The cardinality of a product type is the Product of the cardinalities of it’s constituent types.

For eg. Consider the pair type

data (a, b) = (a, b)

-- |(a, b)| = |a| x |b|

Haskell Records are product-types!

data ExampleRecordType a b = ERT {
  field1 :: a,
  field2 :: Word8,
  field3 :: b
  }

-- |ExampleRecordType| = |a| x |Word8| x |b|
--                     = |a| x 256 x |b|

This would enable us to do rudimentary math with it. You can see how transforming types to numbers, we can do some regular algebra like addition and multiplication with it, an isomorphism would signal equality.

That’s not all folks! We also have another trick up our sleeves.

Exponential types - Functions correspond to Exponentiation (^)

After Sum and Product types, there’s another type that we’d need to know to be effect. These are of the less-known variety and called the Exponential Types.

They aren’t obscure or arcane types you’d never come across, you probably use them everyday!

fun..fun..functions!

That’s right, the function type (->) is the exponential operator analogue of the Types world in Haskell. How so?

Well, it works in the same way an exponential operator (^) would, on regular numbers.

The cardinality of the type a -> b is \(|b|^{|a|}\) where \(|b|\) and \(|a|\) represent the cardinalities of the types a and b respectively.

for eg: The cardinality of a type Bool -> Bool is, \(|2|^{|2|} = 4\), which mean there are only 4 inhabititants of that type. We can also name them if we wanted to:

They are the id, not, const True, and const Not functions.

That may seem it’s around & backwards, why it isn’t \(|a|^{|b|}\) ? It makes more sense when think about it a little different.

For every value of type a that i give, i need a value of type b, but here’s the thing, it can be any value of type b, it won’t matter if a b type value is repeated for different a type values, the mapping a->b doesn’t have to be a 1:1

Which makes looking it as, we get to choose from all b type values, for every value of a type.

\(|a -> b| = \underbrace{ |b| \times |b| \times |b| ….. \times |b|}_\text{a times}\)

\(|a -> b| = |b|^{|a|}\)

Great…

With all that jazz out the way, we can come to using them to see they all work together.

What if i asked you, what’s the cardinality of the type: Either (a, b) (c, d) ?

Calculation steps:-

  • Since we know Either is a sum type, it’s cardinality is a sum of of it’s constituents.
  • Now, the constituent types are both tuples, which are product types, who’s cardinality is product of it’s constituents.

\begin{align*} \text{|} \text{Either (a,b) (c, d)} | &= |(a, b)| + |(c, d)|\\ &= (|a| \times |b|) + (|c| \times |d|) \end{align*}

Which is the sum of products of cardinalities of constituent types here.

Now, suppose we specify those types to concrete types instead of variables:-

data ExampleType = ExampleType
  { number :: Word8,
    isEven :: Bool
  }

To calculate the cardinality of the above type, we start with the outer-most type, which is a Record and make our way inwards. Records are product types:- \[\begin{align*} \text{|} \text{ExampleType} | &= |\text{Word8}| \times |\text{Bool}| \\ &= 256 \times 2 \\ &= 512 \end{align*}\]

The Type “Algebra” in action

FINALLY, we get to use the algebra we learned above into something practical. Understanding and manipulating the algebra behind types gives us options we might not have had otherwise. For. eg.

Consider the example of a TicTacToe board.

data TicTacToe a = TicTacToe
  { topLeft :: a,
    topCenter :: a,
    topRight :: a,
    middleLeft :: a,
    middleCenter :: a,
    middleRight :: a,
    bottomLeft :: a,
    bottomCenter :: a,
    bottomRight :: a
  }
  deriving (Show, Eq)

-- A representation of an empty board

initialBoard :: TicTacToe (Maybe Bool)
initialBoard = TicTacToe
  Nothing Nothing Nothing
  Nothing Nothing Nothing
  Nothing Nothing Nothing

My fingers ached typing that.

Imagine programming against such an thing, writing functions for it or worse, pattern matching on this !

Well, it would have brought many-a-folk on their knees, but not us! We know the mighty secrets of algebra behind types!

The first step here is to do a cardinality analysis on the type. \[\begin{align*} \text{|TicTacToe a|} &= \underbrace {|a| \times |a| \times |a| … \times |a|}_\text{9 times} \\ &= |a|^{9} \\ &= |a|^{3 \times 3} \end{align*}\]

Now, from our knowledge of aglebra behind types, we can see that \(|a|^{3 \times 3}\) has the same cardinality as the type (|3|, |3|) -> |a|. or in it’s curried form |3| -> |3| -> |a|

We can see that we need a type which as cardinality of 3, we can just make one!

data Three = One | Two | Three

now, the same TicTacToe a type can be written as:

data TicTacToeRevised a = TicTacToeRevised {board :: Three -> Three -> a}

emptyBoard :: TicTacToeRevised (Maybe Bool)
emptyBoard = TicTacToeRevised $ const $ const Nothing

The newer revised version is Isomorphic to the previous TicTacToe type! This is much easier to progmram against.

This is what knowing algebra behind types grants us - Freedom -

The Curry - Howard Isomorphism

We saw above the algebraic relation between types and that of their cardinalities. The Curry - Howard Isomorphism generalizes this idea and states that there is a direct relation between logic statements and computer programs. Which means that most math theorems & logic can be expressed as computer programs.

This is summarized in the table below: -

It would probably take a whole another post to explain Curry-Howard in detail, we won’t do it now, but it’s nice to know about it and it’s abstract in the context of this blog post.