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
type class should look like.
One way I use to approach such problems
is to implement instances for the types in
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.
Here is the signature of
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)
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
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
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
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
requires regular functions as input (subtyping goes the other way
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
which doesn’t exist, so pattern matching on it (using the extensions
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, 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
Applicatives. 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 represents uses of the type parameter. It is declared as
newtype Par1 a = Par1 a
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
That means that the prelude
Applicative is also out.
We’re down to either the linear data
Applicative or the linear control
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)
The instances for the datatypes representing multiple constructors (sums)
:+:, composition of type constructors
M1 and reference to other type constructors
R1 just use
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
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)
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
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
Applicative, and this is indeed what
-- newtype K1 i c a = K1 c instance Traversable (K1 i c) where traverse _ (K1 c) = Control.pure (K1 c)
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
class Movable a where move :: a %1-> Ur a
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
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
not a linear control
Applicative! It is only a linear data
pure implementation throws away the argument, so it is not linear. There is an issue
open to add these classes to
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
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!