# Codata and ListT Done Right

When deciding how to implement `ListT`

(the monad transformer) in Haskell, one is tempted to do something like:

`newtype ListT m a = ListT {runListT :: m [a]}`

The problem with this version of `ListT`

is that it does not form a `Monad`

unless the base monad is commutative (i.e. the order of operations does not matter). This rules out potentially useful instances such as `ListT IO`

which you might like to use as a simple streaming interface.

How can we come up with a version of `ListT`

that works? The one above was the only obvious version.

## A Quick Detour, Codata

Data can be thought of as a way of constructing something. A function from a value to a type.

`data A = MkA Int`

Here, the constructor `MkA`

has the type `Int -> A`

Codata, on the other hand, is a way of deconstructing something. That is, we flip the arrows! (This is what “co” tends to mean). So we are looking for something with the type `A -> Int`

instead. Data types in Haskell are actually both data and codata. We even have special syntax for codata. It looks like this:

```
data A = A
getA :: Int
{ }
```

Here, `getA`

has the type `A -> Int`

.

It’s also trivial to convert between a data and codata in Haskell. Basically all we have to do is create a destructor that witnesses every constructor.

For example:

`data A = X Int | Y Char`

can be expressed as

```
data CoA = CoA
getA :: Either Int Char -- Left witnesses X, Right witnesses Y
{ }
```

Side note,

`Either Int Char`

is the same thing as`A`

, so this feels like cheating. Remember, data is codata in Haskell

Back to `List`

. Let’s quickly define it:

`data List a = Cons a (List a) | Nil`

Can we “convert” this to codata?

`data CoList a = CoList { getList :: Maybe (a, CoList a) }`

Here, `Nothing`

witnesses the `Nil`

, and `Just`

witnesses the `Cons`

. Note that we can’t just use the `List`

definition here like we did above because `List`

is a recursive type.

## ListT, with Codata

So, now that we have a codata version of `List`

(which is the same things as `List`

in Haskell, because data is codata), can we come up with a better `ListT`

? Sure, we can do the same trivial thing we tried to do with our regular `List`

definition, just wrap it in the base monad!

`data ListT m a = ListT { runListT :: m (Maybe (a, ListT m a)) }`

Which is exactly `ListT`

done right.

Proving that this forms a monad is left as an exercise to the reader.

It also fits our intuition of what `ListT`

might be for streaming. Each element is produced in the base monad along with the rest of the list.

This corresponds closely with streaming or iterator patterns in other languages. e.g. Rust has the `Iterator`

trait which has the sole method `fn next(&mut self) -> Option<Self::Item>`

which is the same as our `ListT IO`

. The `IO`

is implied, the return type is an `Option`

of the next element, and instead of returning the rest of the list, the list is mutated in place.

So, next time you are struggling to find the correct path forward for your data types, consider thinking about it with the arrows flipped!