# Recursivized Types

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

## Algebraic types

I’ll start with a quick go-over of Haskell types. If you already know Haskell, feel free to skip this section.

### Enumeration types

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

```
data Void
```

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.”

### Structure types

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`

”

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.

### Aside: Kinds

Algebraic types have kinds.

`Singleton`

,`Void`

, and`Bool`

are concrete types in their own right.`Wrapper`

needs a type before it can become a type (nothing can be a`Wrapper`

by itself).`Pair`

needs two types before it can become a type (nothing can be a`Pair`

or`Pair Bool`

by itself).

We refer to the latter two cases as “higher-kinded types.”

We say that `Singleton`

, `Void`

, etc. have kind `*`

. Types that need one type added on the end to be complete, such as `Wrapper`

or `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
```

have kind `* -> *`

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 `True`

.

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 Nil`

, `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 `Null Nothing`

.

## A general encoding of Recursive Types

You might notice a correspondence between the types `Maybe`

and `Nat`

:

```
data Maybe a = Nothing | Just a
data Nat = Zero | Succ Nat
```

Basically, `Nat`

is just `Maybe Nat`

. We can encode the conversion from `Maybe`

to `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 `Recursive Maybe`

.

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
```

Basically, `Zero`

is `Nothing`

and `Succ`

is `Recurse . Just`

, where `.`

is function composition.

Interestingly, there is another possible value of these types

```
omega' = Recurse (Just omega')
omega = Succ omega
```

The name `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`

.

## Recursivizing Types

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 `Recursive Empty`

.

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):

`Recurse Maybe`

\(\equiv\)`Nat`

`Recurse Constant`

\(\equiv\)`Singleton`

`Recurse Wrapper`

\(\equiv\)`Singleton`

`Recurse Empty`

\(\equiv\)`Void`

`Recurse Constant`

\(\equiv\)`Stream`

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 `Recurse`

.

```
data PreList a self = ???
```

And we need to have some element `Nil`

.

```
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)
```

Redoing our `[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\) `List`

.

## Exercises

- 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.

## Conclusion

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`

:-).