Arithmetic on Algebraic Data Types

Per Wikipedia, an algebraic data type is a kind of composite type, i.e., a type formed by combining other types.

Haskell’s algebraic data types are named such since they correspond to an initial algebra in category theory, giving us some laws, some operations and some symbols to manipulate. — Don Stewart

The operations being:

• Sum type = + (data Either a b = Left a | Right b)
• Product type = * (data Product a b = Product a b)
• Function type = ^ (The -> kind in Haskell)

Let |x| denote the number of total possible values that can be constructed of type x. Further let’s assume we have the following types for the example’s sake:

• |Void| = 0 (data Void = in Idris)
• |Unit| = 1 (data () = (), data Unit = Unit)
• |Bool| = 2 (data Bool = True | False)
• |Maybe a| = |a| + 1 (data Maybe a = Just a | Nothing)

From here, let’s see how we can use the operations with these symbols.

Sum type example #1

We have |Either a b| = |a| + |b| in general, so for |Either Unit Bool| we have |Unit| + |Bool| which is 3. The values being: Left Unit, Right True, Right False.

Product type example #2

We have |Product a b| = |a| * |b| in general, so for |Product Bool Bool| we have |Bool| * |Bool| which is 4. The values being: Product False False, Product False True, Product True False, Product True True.

Exponentiation type example #3

We have |a -> b| = |b|^|a| in general, so for |Maybe Bool -> Bool| we have |Bool|^|Maybe Bool| which is |Bool|^(|Bool| + 1) or simply 8. The values being:

1. f Nothing      = False
   f (Just True)  = False
   f (Just False) = False
   

2. f Nothing      = False
   f (Just True)  = False
   f (Just False) = True
   

3. f Nothing      = False
   f (Just True)  = True
   f (Just False) = False
   

4. f Nothing      = False
   f (Just True)  = True
   f (Just False) = True
   

5. f Nothing      = True
   f (Just True)  = False
   f (Just False) = False
   

6. f Nothing      = True
   f (Just True)  = False
   f (Just False) = True
   

7. f Nothing      = True
   f (Just True)  = True
   f (Just False) = False
   

8. f Nothing      = True
   f (Just True)  = True
   f (Just False) = True
   

Cool, right? 🙂

EDIT: Thanks to u/princessOfApple for pointing out an error in the product example.