So, a short break from \(\varepsilon—\delta\).
Anyway, I’m going to look at Algebraic types in this section. Specifically, I am going to use Haskell types.
The provided code is all actual Haskell, in fact, I’m going to have to de-import the standard libraries because some of this is actually defined there. You can find all the code here
I’ll start with a quick go-over of Haskell types. If you already know Haskell, feel free to skip this section.
Some types are enumerations of potential values.
A quick example is the trivial singleton type:
data Singleton = Single deriving Show
This is to be read as “there exists a type Singleton, which contains one element named Single.” The “deriving show” part is Haskell book keeping for those following along on their interpreters to be able to see things
Another example is
This is to be read as “there exists a type Void with no possible elements”
Yet another type is
data Bool = False | True deriving Show
This is to be read as “there exists a type Bool with the possible elements True and False.”
Types can be used as as structures, as such:
data Wrapper a = Wrap a deriving Show
This is to be read as “for every type
a there exists a type
(Wrapper a) with a single type constructor
Wrap that takes an
A more complicated structure is
data Pair a b = ConsPair a b deriving Show
Which is similar to the previous one except that it contains two possible elements which can be of two different types.
Algebraic types have kinds.
Boolare concrete types in their own right.
Wrapperneeds a type before it can become a type (nothing can be a
Pairneeds two types before it can become a type (nothing can be a
Pair Boolby itself).
We refer to the latter two cases as “higher-kinded types.”
We say that
Void, etc. have kind
*. Types that need one type added on the end to be complete, such as
Pair Bool have kind
* -> *. Types such as
Pair, which needs two types to be complete, have kind
* -> * -> *.
Note also that types such as
data TwoOfSame a = ConsTwoOfSame a a
* -> * rather than
* -> * -> * because they only take one type argument.
TwoOfSame Bool Singleton wouldn’t make any sense.
Mixing Structures and Enumerations
Algebraic types are a generalization of both systems, in which you can have multiple constructors, each of which can contain zero or multiple arguments.
A canonical example combines both forms to create something resembling the concept of
null from Java or
None from Python.
data Maybe a = Nothing | Just a deriving Show
Here, there is a combination of the enumeration and structure style. Interestingly, while, for example,
Just True :: Maybe Bool (
:: is to be read as “is of type”),
Nothing :: Maybe a, which means that it can take on any
Just type (this is key to what we will do later).
Recursive Algebraic types
Recursive types are similar to the examples shown, except that they can also contain themselves. For example, the not particularly efficient definition of the natural numbers (a natural number is either zero or the successor of another natural number):
data Nat = Zero | Succ Nat deriving Show
Another algebraic type is a stream, which is defined as follows, which is basically an infinite list.
data Stream a = ConsStream a (Stream a) deriving Show
This only works because you can define values as follows, where in each case the same variable name refers to the same value:
trues = ConsStream True trues falses = ConsStream False falses alternating = ConsStream True (ConsStream False alternating) elementAt (ConsStream value rest) Zero = value elementAt (ConsStream value rest) (Succ x) = elementAt rest x
So if you ask for the (fifth element of trues), that reduces to the (fourth element of (the rest of trues)) which reduces to (the fourth element of trues), etc., until you get to the value
A potentially terminating list can be represented as follows:
data List a = Nil | Cons a (List a) deriving Show
Here the list can possibly terminate because you can stop with
Nil. For example, you can represent
[True, False, False] as
exampleList = Cons True (Cons False (Cons False Nil))
You could also use stream-like circular definition for a list too, so streams are just a subset of lists.
Higher-kinded type parameters
OK, one final bit of craziness before we get to our actual example. Let’s say we want to create a type representing the shape of another type.
data Shape f = Structure (f Singleton)
If we, for example, look at
Shape List, we get the values
Structure (Cons Single Nil),
Structure (Cons Single (Cons Single Nil)), etc. Basically, we get a picture of what the type looks like independent of its elements.
Notice that on the right side of that equation we have
(f Singleton) as a concrete value, meaning that
f is of kind
* -> *. Therefore,
Shape is of kind
(* -> *) -> *.
Another example of a
(* -> *) -> * is the
NullOf type, which filters a type for only its nullary constructors, those which do not take a value.
data NullOf f = Null (f Void)
For example, the only possible value of
NullOf List is
Null Nil and the only possible value of
NullOf Just is
A general encoding of Recursive Types
You might notice a correspondence between the types
data Maybe a = Nothing | Just a data Nat = Zero | Succ Nat
Nat is just
Maybe Nat. We can encode the conversion from
Nat as follows:
data Recursive f = Recurse (f (Recursive f))
This definition means that for all types
f of kind
* -> *, there exists a type called
Recursive f (let’s call this
rf for now) which contains a single element whose type is
f rf. In other words,
Recursive takes a type and returns a recursive version of that type.
Constructing a value of
Recursive * at first seems difficult. For example, let us look at
To construct a type of
Recursive Maybe we need to have an element of type
Maybe (Recursive Maybe). The only element of this we have is
Nothing :: Maybe a. We can therefore construct the value
Recurse Nothing :: Recursive Maybe. Using this value we can construct the value
Just (Recurse Nothing) :: Maybe (Recursive Maybe) and therefore the value
Recurse (Just (Recurse Nothing)) :: Recursive Maybe. We can continue to build values in this manner:
zero' = Recurse Nothing one' = Recurse (Just zero') two' = Recurse (Just one') three' = Recurse (Just two')
Notice that I used the names for numbers for these. This is to demonstrate their correspondence with the natural numbers:
zero = Zero one = Succ Zero two = Succ one three = Succ two
Recurse . Just, where
. is function composition.
Interestingly, there is another possible value of these types
omega' = Recurse (Just omega') omega = Succ omega
omega is used because this number is similar to one particular kind of infinity. because of the way that it reacts to this definition of comparison:
_ < Zero = False Zero < Succ _ = True Succ x < Succ y = x < y
As you can see,
x < omega is
True for all
x defined by
Succ (Succ (Succ ... Succ (Zero))). Note that
omega < omega will never evaluate since
omega < omega reduces to
Succ omega < Succ omega, which reduces to
omega < omega.
To begin with, let’s look at the entirely contrived types:
data Constant a = Const deriving (Show) data Empty a
We can see that there is one possible value for
Constant (Recursvie Constant), which is
Const. Therefore, the only possible value for
Recursive Constant is
Recurse Const. Therefore,
Recursive Constant is similar to the Singleton:
single = Single single' = Recurse Const
Similarly, there is no value
Empty (Recursive Empty) possible, so there is no possible value of
Let’s now look at a less contrived
* -> * type, Wrapper, and see how it works.
Recursive Wrapper requires a value of
Wrapper (Recursive Wrapper) in order to initialize. There is in fact only one way to do this:
wrappedRecurse = Recurse (Wrap wrappedRecurse)
This type is also basically
Singleton since it only has one value
We can also use the partial application of
Pair to a single type variable
a and then construct a recursion of the pair. We can then analyze values of
Recurse (Pair Bool). At first, this doesn’t seem to work any better than
Recurse Wrap because we need a value of
Pair Bool (RPair Bool) before we can create a value of
RPair Bool. However, since in this case each value also has a
Bool, these form a stream:
trues' = Recurse (ConsPair True trues') falses' = Recurse (ConsPair False falses') alternating' = Recurse (ConsPair True (Recurse (ConsPair False alternating')))
Which is remarkably similar to our previous definitions:
trues = ConsStream True trues falses = ConsStream False falses alternating = ConsStream True (ConsStream False alternating)
Finding the base type for recursive types
So now we know (I’m using \(\equiv\) to mean that two types have the same structure):
But what is
List equivalent to? We can look again at the definition of a list:
data List a = Nil | Cons a (List a)
OK, so we need to have a type parameter representing the
a and another to be eaten by
data PreList a self = ???
And we need to have some element
data PreList a self = PreNil | ???
Now, we just need something to combine both the first and rest of the list
data PreList a self = PreNil | PreCons a self
Hey, what’s on the right of the list looks a lot like a
Maybe with two values instead of one! Here’s a final implementation
data PreList a self = PreList (Maybe (Pair a self)) deriving (Show) type RecurseList a = Recursive (PreList a)
[True, False, False] example, we get:
exampleList' = Recurse (PreList (Just (ConsPair True (Recurse (PreList (Just (ConsPair False (Recurse (PreList (Just (ConsPair False (Recurse (PreList Nothing)))))))))))))
No reasonable person (except (maybe (a (Lisp (fanatic))))) would say that the above code is pretty, but it is clear that
Recursive (PreList a) \(\equiv\)
- Find the de-recursified forms of
data BinaryTree a = BNode (BinaryTree a) (BinaryTree a) | BLeaf a data ListTree a = ListNode a (List (ListTree a))
- What is a general algorithm for de-recursification?
The answers are given at the end of the attached source code.
OK, so this probably doesn’t have any practical applications. And given how ugly the output of such code is, you’re unlikely to ever see this in real life code, even in an academic language like Haskell.
On the other hand, I hope this hurt your brain a little; it certainly hurt mine. Really, to me, the best part is that with only a simple type system (e.g., non-recursive types), and a single recursive type, you can construct all other simply recursive types. This example shows to me how out of simplicity can grow complexity.
Also, abstract nonsense is
Just fun :-).