Tuesday, January 3, 2012

Haskell for Intermediate Programmers - Algebraic Data Types

Haskell uses "algebraic" data types, but none of the tutorials or introductions really explain why they are called "algebraic". Let's go over the real origin of their name and perhaps gain a deeper understanding of them.

Algebraic data types are types that can be modeled using simple algebra, namely addition and multiplication. Wait, what? I can add types? Yes:
a + b = Either a b
Addition is associative, and Eithers are "sort of" associative, which is to say that if we squint, the following two types are essentially the same:
Either (Either a b) c ~ Either a (Either b c)
(a + b) + c = a + (b + c)
... where I use ~ to denote "essentially the same". We can show they are equivalent by creating functions that transform each type to the other:
forward  x = case x of
    Left  e -> case e of
        Left  a -> Left a
        Right b -> Right (Left b)
    Right c -> Right (Right c)
reverse x = case x of
    Left  a -> Left (Left a)
    Right e -> case e of
        Left  b -> Left (Right b)
        Right c -> Right c

-- or more tersely:
forward  = either (either Left (Right . Left)) (Right . Right)
reverse = either (Left . Left) (either (Left . Right) Right)
We can also multiply types:
a * b = (a, b)
This is also associative:
((a, b), c) ~ (a, (b, c))
(a * b) * c = a * (b * c)

forward  ((a, b), c) = (a, (b, c))
reverse (a, (b, c)) = ((a, b), c)
More importantly, multiplication distributes over addition, just like in normal algebra:
(a, Either b c) ~ Either (a, b) (a, c)
a * (b + c) = a * b + a * c

forward (a, e) = either (Left . (a ,)) (Right . (a ,)) e
reverse = (either fst fst, either (Left . snd) (Right . snd))
We can also create an analog of 0:
data Zero -- a data type with no constructor

Either Zero a ~ a
0 + a = a

forward (Right a) = a
reverse a = Right a -- or reverse = Right
The forward function doesn't need to check the alternative case for the Left constructor because we can't create a value of type Zero.

The analog of 1 is any type with a single empty constructor, such as the () type:
type One = ()
(One, a) ~ a
1 * a = a

forward (One, a) = a
reverse a = (One, a)
Multiplying by Zero has the expected effect:
(Zero, a) ~ Zero
0 * a = 0

-- Neither type can be built
Incredibly, we can "essentially" create any Haskell data type using only Either, (,), (), and Zero. Some examples of Haskell types and their algebraic equivalents:
data Bool = True | False
Bool ~ 1 + 1 -- i.e. Either () ()
     = 2

data Maybe = Just a | Nothing
Maybe a ~ a + 1 -- i.e. Either a ()

data Trool = True_ | False_ | Empty -- "troolean"
Trool ~ 1 + 1 + 1 -- i.e. Either (Either () ()) ()
      = 3

-- or
type Trool = Maybe Bool
Trool ~ Bool + 1 -- i.e. Either (Either () ()) ()
      ~ 2 + 1
      = 3

data TwoBools = TwoBools Bool Bool
TwoBools ~ Bool * Bool -- i.e. (Bool, Bool)
         ~ 2 * 2
         = 4
Each type corresponds to an algebraic number which tells us how many states that type can represent. The Bool type represents 2 states. The two Trool types represent 3 states.

This state-counting explains why the algebraic equivalence works: If two types represent the same number of states, you can always reversibly convert them back and forth. When we multiply two types, we multiply the number of states they represent. When we add two types, we add the number of states they represent.

We can follow some simple rules to translate Haskell data types into algebraic expressions:
  • Replace | with +
  • Replace a constructor (or tuple) that holds multiple values with a product
  • Replace an empty constructor with 1.
  • Replace a type with no constructor with 0
For example:
data Sum a b c = S1 a | S2 b | S3 c
Sum a b c ~ a + b + c

type Sum2 a b c = Either a (Either b (Either c Zero)))
Sum2 a b c = a + (b + (c + 0))
           = a + b + c

data Product a b c d e = P a b c d e
Product a b c d e ~ a * b * c * d * e

type Product2 a b c d e = (a, b, c, d, e)
Product2 ~ a * b * c * d * e

type Product3 a b c d e = (a, (b, (c, (d, (e, ())))))
Product 3 ~ a * (b * (c * (d * (e * 1))))
          = a * b * c * d * e

data Term a b c = T1 a b | T2 c 
Term a b c ~ a * b + c

type Term2 a b c = Either (a, b) c
Term2 a b c ~ a * b + c
In the above example, we can think of the type constructors as algebraic functions. Sum computes the sum of its three arguments. Product computes the product of its five arguments.

But what about recursive types? They work, too!
data List a = Nil | Cons a (List a)
List a ~ 1 + a * List a
       ~ 1 + a * (1 + a * List a)
       ~ 1 + a * (1 + a * (1 + a * List a))
       ~ ...
       ~ (1) + (a) + (a * a) + (a * a * a) + ...
This tells us that a List is either empty (1) or (+) has 1 element (a) or (+) has 2 elements (a * a) or (+) has 3 elements (a * a * a) and so on. That's pretty slick!

So far I've only mentioned algebraic equivalents to data types, but we can even represent functions as algebraic expressions:
a -> b = b ^ a
To see why, imagine that our function has a finite domain (i.e. a has n possible states, where n is finite). Then, we could encode our function by just asking what will its result be for all possible values of a and storing those results in an n-tuple.

For example, if we write a function of type Bool -> Trool, then we could instead rewrite our function as a simple data type of type (Trool, Trool) (one Trool for each state of Bool). This immediately tells us that there are only 9 unique functions with that type, and the algebraic translation agrees:
Bool -> Trool ~ Trool^Bool
              ~ 3^2
              = 9
For example, if our function were:
data Trool = True_ | False_ | Empty

f :: Bool -> Trool
f x = case x of
    True -> Empty
    False -> False_
I could instead encode that function as a tuple, as long as I use a consistent encoding/decoding convention:
f' :: (Trool, Trool)
f' = (Empty, False_)

f' ~ f
If -> really exponentiated types, we'd expect the following two types to be essentially equal:
a -> b -> c ~ (a, b) -> c
(c^b)^a = c^(a * b)

forward = uncurry
reverse = curry
... and they are!

Obviously, we work with many types that do not have a finite number of states, such as Integer or List a, but it doesn't mean the algebra is wrong. It's just that now we are adding and multiplying infinities, so we will always get an infinite number of possible states. However, the algebra still gives us a good intuition of how we can "essentially" construct any type just from just two base types and three orthogonal functions on types:
-- Base types
data Zero
type One = ()

-- Type Functions
a + b = Either a b
a * b = (a, b)
a -> b = b^a
Unfortunately, an "essentially equal" type won't cut it in Haskell, since it won't type-check, but I hope this helps explain some of the motivation behind Haskell's data type system.

It would be really elegant if Haskell's type system was just syntactic sugar on top of the above minimal type system. In other words, alternate constructors would just get translated into a sum fold:
data For = A a | B b | C c
-- gets translated into
newtype For = For
    { unFor :: Either a (Either b (Either c Zero))) }
... and constructors that contained several values would get translated into a product fold:
data All = A a b c d e
-- gets translated into
newtype All = All
    { unAll :: (a, (b, (c, (d, (e, ()))))) }
It would be even nicer if these newtypes could automatically derive class instances from their components types based on the algebra (i.e. a more powerful version of GeneralizedNewtypeDeriving). To elaborate, just imagine having a type H that was an instance of some interface:
class HasHeight t where getHeight :: t -> Double

instance HasHeight H where getHeight = ...
Then you define some other type based off of H:
data Object x y = Person H x | Building H y | Chair H
    deriving (HasHeight)
Then the class system does some algebra behind the scenes to confirm that it can treat Object as a super-set of H:
Object x y = H * x + H * y + H
               = H * (x + y + 1) -- confirmed!
Then it automatically derives the instance:
instance HasHeight Object where
    getHeight o = case o of
        Person   h _ -> getHeight h
        Building h _ -> getHeight h
        Char     h   -> getHeight h
Unfortunately, Haskell's class system isn't strong enough to express this kind of behavior, so we are stuck bickering over various record implementations instead of enjoying a truly algebraic type system.

No comments:

Post a Comment