The design of a library like `linear-base`

, Tweag’s standard library for Haskell’s
linear types, requires many choices.
One of these choices for `linear-base`

is what a linear `Traversable`

type class should look like.

One way I use to approach such problems
is to implement instances for the types in `GHC.Generics`

.
`GHC.Generics`

provides a way to implement datatype-generic functions by translating a datatype to and from
a limited set of primitive datatypes representing sums, products, constants, etc.
Therefore, a type class implemented for this set can be given an
instance at a large class of algebraic datatypes.
So this is a nice way to apply structural reasoning to a problem.

## The problem

Here is the signature of `fmap`

in `linear-base`

, as it applies, for instance, to lists:

```
-- The syntax for linear functions is `%1->`.
-- Linear functions consume their input exactly once.
fmap :: (a %1-> b) -> t a %1-> t b
```

Correspondingly, it seems pretty clear that the type of linear `traverse`

should be:

`traverse :: Applicative f => (a %1-> f b) -> t a %1-> f (t b)`

But which `Applicative`

type class should we use? In the context of linear types, there are three different ones! The one from the prelude:

```
Prelude.pure :: a -> f b
Prelude.fmap :: (a -> b) -> (f a -> f b)
Prelude.liftA2 :: (a -> b -> c) -> (f a -> f b -> f c)
```

And two linear ones: a linear *data* `Applicative`

:

```
Data.pure :: a -> f b
Data.fmap :: (a %1-> b) -> (f a %1-> f b)
Data.liftA2 :: (a %1-> b %1-> c) -> (f a %1-> f b %1-> f c)
```

and a linear *control* `Applicative`

:

```
Control.pure :: a %1-> f b
Control.fmap :: (a %1-> b) %1-> (f a %1-> f b)
Control.liftA2 :: (a %1-> b %1-> c) %1-> (f a %1-> f b %1-> f c)
```

Note that I’m leaving out `<*>`

. Its type signature hides a nice symmetry, and can be defined as `liftA2 ($)`

in all cases.

Another thing to note is that any linear function is also a regular function, which means that any linear *control* `Applicative`

is also a linear *data* `Applicative`

, so the latter is a superclass
of the former. On the other hand, neither linear `Applicative`

is a subclass (or superclass)
of the prelude `Applicative`

, since they can be given linear functions as input, while prelude `Applicative`

requires regular functions as input (subtyping goes the other way
for inputs).

## Instances of `GHC.Generics`

datatypes

`V1`

Let’s start by writing an instance for `V1`

, which represents empty data types. Such instances are usually either easy or impossible
to implement. In this case we’re lucky since callers of `traverse`

are supposed to provide a value of type `V1 a`

,
which doesn’t exist, so pattern matching on it (using the extensions `LambdaCase`

and `EmptyCase`

) is all we need to do.
There’s also no need for any `Applicative`

method, so we don’t learn anything either.

```
-- data V1 a
instance Traversable V1 where
traverse _ = \case
```

`U1`

Next is `U1`

, which represents constructors with no fields. We get a value of type `U1 a`

and need to produce a value of type `f (U1 b)`

.
We can produce values of type `U1 b`

for any `b`

out of thin air, and by applying `pure`

, linear or not, we get the desired `f (U1 b)`

.
So this works for all 3 `Applicative`

s. But note that the linearity forces us to pattern match on the input
to prove that we completely consume it. Just `traverse _ _ = pure U1`

does not work.

```
-- data U1 a = U1
instance Traversable U1 where
traverse _ U1 = pure U1
```

`Par1`

The constructor `Par1`

represents uses of the type parameter. It is declared as

`newtype Par1 a = Par1 a`

and `traverse`

at this type is:

`traverse :: (a %1-> f b) -> (Par1 a %1-> f (Par1 b))`

We’re going to implement this in roughly the following way:

`traverse g (Par1 a) = let fb = g a in fmap Par1 fb`

Since we’re promising to use `Par1 a`

linearly, every step needs to be linear.
We pattern match to get an `a`

, apply the input function of type `a %1-> f b`

and get `fb :: f b`

linearly.
But we need `f (Par1 b)`

, so we apply `fmap Par1`

. But `fmap`

from the Prelude isn’t linear,
it does not promise to use `fb`

exactly once, so we can’t use it here for linear `Traversable`

!
That means that the prelude `Applicative`

is also out.

We’re down to either the linear *data* `Applicative`

or the linear *control* `Applicative`

.
Thanks to the superclass relation between the two we can use the `Data`

one here in both cases:

```
instance Traversable Par1 where
traverse g (Par1 a) = Data.fmap Par1 (g a)
```

`:+:`

, `:.:`

, `M1`

, `Rec1`

The instances for the datatypes representing multiple constructors (sums) `:+:`

, composition of type constructors `:.:`

,
meta information `M1`

and reference to other type constructors `R1`

just use `fmap`

and don’t provide any new information.

```
-- data (l :+: r) a = L1 (l a) | R1 (r a)
instance (Traversable l, Traversable r) => Traversable (l :+: r) where
traverse f (L1 la) = Data.fmap L1 (traverse f la)
traverse f (R1 ra) = Data.fmap R1 (traverse f ra)
-- newtype (s :.: t) a = Comp1 (s (t a))
instance (Traversable s, Traversable t) => Traversable (s :.: t) where
traverse f (Comp1 sta) = Data.fmap Comp1 (traverse (traverse f) sta)
-- newtype M1 i c t a = M1 (t a)
instance Traversable t => Traversable (M1 i c t) where
traverse f (M1 ta) = Data.fmap M1 (traverse f ta)
-- newtype Rec1 t a = Rec1 (t a)
instance Traversable t => Traversable (Rec1 t) where
traverse f (Rec1 ta) = Data.fmap Rec1 (traverse f ta)
```

`:*:`

In the case of the product `(:*:)`

, we need to combine two `Applicative`

values using `liftA2`

.
Again we have to do this linearly so the prelude `Applicative`

does not work, but the two linear ones do.

```
-- data (l :*: r) a = l a :*: r a
instance (Traversable l, Traversable r) => Traversable (l :*: r) where
traverse f (la :*: ra) = Data.liftA2 (:*:) (traverse f la) (traverse f ra)
```

`K1`

We have one more datatype left to do, `K1`

for constants. We have an input value of type `K1 i c a`

and need
to produce a value of type `f (K1 i c b)`

. We can pattern match on the input to get the constant of type `c`

out,
and apply the `K1`

constructor again to produce a value of type `K1 i c b`

. Next we can apply `pure`

to get the
desired result, but we need to do so linearly and `Data.pure`

is not linear! So we’re left with just the linear
*control* `Applicative`

, and this is indeed what `linear-base`

provides.

```
-- newtype K1 i c a = K1 c
instance Traversable (K1 i c) where
traverse _ (K1 c) = Control.pure (K1 c)
```

## An alternative

We couldn’t use `Data.pure`

because it doesn’t consume its input linearly, and we can use the constant just once.
But what if we could use the constant more than once? This is exactly what `Movable`

from `linear-base`

provides!

```
class Movable a where
move :: a %1-> Ur a
```

Here `Ur a`

(`Ur`

stands for unrestricted) gives unlimited access to values of type `a`

, even in linear context.
So if we have an instance of `Movable`

for the constant we *can* use `Data.pure`

, and therefore it seems useful
to also have a version of `Traversable`

that uses the linear *data* `Applicative`

.

```
instance Moveable c => Traversable (K1 i c) where
traverse _ (K1 c) = move c & \case (Ur c') -> Data.pure (K1 c')
```

This would lead to instances like:

```
instance Movable a => Traversable (Either a)
instance Movable a => Traversable ((,) a)
```

Is having two different `Traversable`

classes worth it? It seems so, for at least one particular reason:
`Foldable`

can be shown to be derived from `Traversable`

using the `Const`

`Applicative`

. But `Const`

is
not a linear *control* `Applicative`

! It is only a linear *data* `Applicative`

,
because its `pure`

implementation throws away the argument, so it is not linear. There is an issue
open to add these classes to `linear-base`

.

## Conclusion

One final thought (and you might have been wondering about this) now that we have instances of `Traversable`

for all
`GHC.Generics`

datatypes: can we generically derive instances of linear `Traversable`

? Well, there is one catch. The
`to1`

and `from1`

methods from the `Generic1`

class that are needed are not linear! They should be in principle, since
instances are not supposed to throw stuff out nor duplicate anything either. But we can’t be sure, so for now we can
only provide generic instances using `Unsafe.toLinear`

with a big fat warning sign.
(We’re still working out the best way to do so.)

I hope you enjoyed this exploration of linear traversals over the zoo of `GHC.Generics`

datatypes as much as I did.
I encourage you to play with linear types a bit, it can be really surprising what works and what doesn’t work linearly!