# Lambdas are Codatatypes

1 July, 2019

I was first clued into this a while ago by a comment on Bob Harper’s blog that “exponentials are coinductive”, but it only really clicked for me today. Let’s get into it.

## Datatypes

### Defining them

When you define a datatype, you list the ways to construct values of that type. For example, this definition:

```
data Bool : Type where {
True;
False
}
```

says there are two ways to construct a `Bool`

: `True`

and `False`

.

Similarly, this definition:

```
data These (a : Type) (b : Type) : Type where {
This[a];
That[b];
These[a, b]
}
```

gives three ways to construct a `These a b`

(for any values of `a`

and `b`

). `This[0]`

has type
`These Int x`

, for any `x`

. `That[True]`

has type `These x Bool`

for any `x`

. `These[0, True]`

has
type `These Int Bool`

.

I want to note that constructors aren’t functions; they have a fixed number of arguments and must be fully applied.

Datatypes can also be defined recursively:

```
data List (a : Type) : Type where {
Nil;
Cons[a, List a]
}
```

### Using them

The way you construct a value of a datatype is unique to that datatype; there are a finite number of
constructors, and each represents a different way to build a value of that type. In contrast, there is
a universal way to *destruct* values: pattern matching.

If some expression `x`

has type `Bool`

then we can destruct `x`

using pattern matching:

```
case x of {
True -> ...;
False -> ...
}
```

A pattern match acknowledges all the ways that a value could have been constructed, and provides
a branch for each possible case. When constructors carry around other values
(like those of `These`

or `List`

), pattern matching is used to write programs that extract and
process the inner values:

```
case y of {
This[a] -> f a;
That[b] -> g b;
These[c, d] -> h c d
}
```

When a program is running, the value that is being matched will eventually reduce to a constructor form:

```
case (These 0 True) of {
This[a] -> f a;
That[b] -> g b;
These[c, d] -> h c d
}
```

at which point, the appropriate branch is selected and the contents of the constructor are substituted
to the right of the `->`

. The above code will pick the `These`

branch, substituting `0`

for `c`

and `True`

for `d`

, so that the final result is `h 0 True`

.

Pattern matching is enough to process non-recursive datatypes, but recursive datatypes require recursive function definitions:

```
sum : List Int -> Int
sum n =
case n of {
Nil -> 0;
Cons[x, xs] -> x + sum xs
}
```

Hopefully this is all familiar to you. I’ve covered all this so that it contrasts with *codatatypes*.

## Codatatypes

Codatatypes are the dual to datatypes. Formally, this means a lot of things that I don’t yet understand. What follows is how this duality arises in practise.

To begin, I’d like to share some hand-wavy intuition for the concepts I’m discussing.

Datatypes *are*. They’re finite, fully-evaluated structures. They’re inert; they just exist and won’t ever
“do anything”. Haskell doesn’t have true ‘datatypes’ in this sense because its constructors don’t force their
arguments to be evaluated, which means you can hide computations inside them. Haskell lets you partially
apply constructors, which further diverges from what I’ve laid out here.

Codatatypes *do*. They have ‘potential energy’; they have the capacity to do more work when prodded. Haskell’s
‘datatypes’ are more codata-like in this respect because they can contain suspended computations.

### Defining them

Since datatypes are defined by their constructors, codatatypes will be defined by their *destructors*.

This definition:

```
codata Pair (a : Type) (b : Type) : Type where {
fst : a;
snd : b
}
```

says that there are two ways to *destruct* a `Pair a b`

(for any `a`

and `b`

). If some expression `x`

has
type `Pair a b`

, then `x.fst`

has type and `a`

, and `x.snd`

has type a `b`

.

`Pair`

really is pair, it has just been defined by the ways you can pull things out of it- you can either
extract the first thing, or you can extract the second.

I also want to note that destructors aren’t functions, either. You can’t partially apply a destructor, and they’re not first-class.

Codatatypes can also be recursive:

```
codata Stream (a : Type) : Type where {
head : a;
tail : Stream a
}
```

A stream is like an infinite list; every stream value contains a head and a tail, and no matter how many times you extract the tail, there will always be another stream waiting for you.

### Using them

There is a universal way to destruct datatypes, and there is a universal way to *construct* *codatatypes*.
For lack of a better term, you can call it ‘copattern matching’. Here’s how you would construct a
`Pair Int Bool`

:

```
cocase Pair Int Bool of {
fst -> 0;
snd -> True
}
```

A copattern match acknowledges every way it could be destructed, and provides a branch for each case.
Remember, copattern matching *constructs* values. The above code is a value that produces `0`

when
destructed using `fst`

, and `True`

when destructed using `snd`

. It is defining a pair of `0`

with `True`

.

When a program is running, a value that is being destructed will eventually reduce to a copattern match form.
So `x.fst`

might reduce to `(cocase Pair Int Bool of { fst -> 0; snd -> True }).fst`

. At this point,
the appropriate branch in the copattern match will be chosen, and the right hand side of the `->`

will be
selected. In this case, `(cocase Pair Int Bool of { fst -> 0; snd -> True }).fst`

reduces to `0`

.

Recursive codatatypes like `Stream`

need to be constructed by recursive definitions:

```
countFrom : Int -> Stream Int
countFrom n =
cocase Stream Int of {
head -> n;
tail -> countFrom (n+1)
}
```

`countFrom 0`

produces an infinite stream of integers starting at `0`

. However, it doesn’t spin forever,
trying to construct the entire stream in one go. This is because a lone copattern match won’t reduce; reduction
only continues after a destructor has been applied and the correct branch has been selected. Because of
this, codatatypes can represent infinite values that are only generated on demand.

Datatype constructors can carry around values, and so can codatatype *destructors*.
Here’s what that looks like:

```
codata Lambda (a : Type) (b : Type) : Type where {
apply[a] : b
}
```

There is one way to destruct a value of type `Lambda a b`

called `apply`

, and this destructor takes a
parameter. If `f`

has type `Lambda a b`

, and `x`

has type `a`

, then `f.apply[x]`

has type `b`

.

To create a value of type `Lambda a b`

, you would use a copattern match:

```
cocase Lambda a b of {
apply[x] -> ...
}
```

The destructor’s parameter is abstract and is to be filled by the value that the destructor will be carrying.
For example, `(cocase Lambda Int Int of { apply[x] -> x + 1 }).apply[2]`

selects the appropriate branch
(there’s only one), and substitutes `2`

for `x`

to the right of the `->`

. It steps to `2 + 1`

.

So lambdas can be defined as codatatypes. Their destructor corresponds to function application, and copattern matching corresponds to abstraction. This is awesome!