-
Notifications
You must be signed in to change notification settings - Fork 37
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The Traversal story #220
Comments
Cc @b-mehta , you may be interested in opining. |
I'm assuming, here, that traversals are built from the same type as `Traverse`. I believe this to be the right type, which I explain in some details in #220.
I'm assuming, here, that traversals are built from the same type as `Traverse`. I believe this to be the right type, which I explain in some details in #220.
It occurred to me that I can probably give a But if I do that, then, when I do an unrestricted traversal, I will pay the reification for each call of If, on the other hand, we define the unrestricted traversal for the linear Kleisli by reifying the linear |
The This is why the Bazaar a b t = forall f. Applicative f => (a %1 -> b) -> f t (The irrelevant Context a b t = forall f. Functor f => (a %1 -> b) %1 -> f t I leave it to you to map onto Control and Data Applicative, the names still trip me up as to which is which ;) Linear versions of those should translate directly. With all the same instances as
can never even start to assemble a |
Let me write some thought on the design of optics, and especially
traversals, so that I don't forget again. All this should make its way
into a document
Profunctor optics
When designing the optics library, I settled on profunctor optics
rather than a Van Laarhoven encoding for two reasons:
require some profunctoriness, which the lens library has to work around)
newtype
forOptic_
thateverything else is a restriction on.
As I'm writing this, I realise that we could have done
newtype Optic_ p f s t a b = Optical (p a (f b)) -> p s (f t))
and defined, say,lens as
type Lens s t a b = forall f. Functor f => Optic (FUN 'One) s t a b
), which counter the second point, but as I'm writing thiscounter, another benefit of profunctors is coming back:
FUN 'One
vs(->) = FUN 'Many
.The latter is used in lens for instance so that
over
can be linearwhile
get
andset
aren't. If we forcedFUN 'One
, thenset
andget
would still be definable, but would require additionalallocations, which would be a bit unfortunate.
So, anyway, profunctor it is. Not that it makes the problem of
Traversal
any harder really, so whatever.Traversals
The first difficulty with traversals is that they can be defined in
two ways. Let me define a bunch of classes on profunctors:
Both
Strong
super-classes are implied bywander'
since both(c,)
and
Either c
are traversable.Dilemma
The first difficulty that we face is that there are two different
definitions for profunctor traversable in the literature.
Traversal s t a b = Optic (\p. (Strong (,) () p, Strong Either Void p, Monoidal (,) () p))
as in the 2017 profunctor optics paperTraversal s t a b = Optic (Wandering p)
as in the Purescriptprofunctor lens library
These two definitions are equivalent (and are equivalent to a bunch
of other definitions not involving profunctors, like the Van Laarhoven
encoding). However, I don't believe that
(Strong (,) () p, Strong Either Void p, Monoidal (,) () p)
andWandering p
are equivalent!In fact I don't believe either is included in the other (but I don't
have a proof), I'm at least pretty sure that
Wandering p
doesn'timply
Monoidal (,) () p
.So it's a true choice. We could even require
(Monoidal (,) () p, Wandering p)
, or makeMonoidal (,) () p
a super class ofWandering p
. There are a lot of possible choices.The intuitive reason why all of these things work is that the only
profunctor which really matters for traversals is
for
f
a control applicative functor. And it has all of the aboveinstances. So, whatever instances we choose, we can define
traverseOf
easily and efficiently.Van Laarhoven encodings are great at defining traversals
Where things are more difficult is for defining traversals. Let's give
ourselves an example type.
Definining a Van-Laarhoven-style traversal is as easy as:
It's very terse. Very readable. Very systematic. Very exactly what we
want.
If you try defining the same traversal with just
(Strong (,) () p, Strong Either Void p, Monoidal (,) () p)
you are not going to havefun. First you will notice that you kind of want
Monoidal Either Void
as well (which, to be fair, we could throw in no problem).With
Wandering
we have, instead,It's almost as easy as in the Van Laarhoven case. Not quite perfect,
but quite ok. (note: if we had
wander'
and notwander
this wouldbe rather non-fun again)
Which is, I assume, is the reason why Purescript uses this definition.
Unrestricted traversals
I lied above. There is a second profunctor of interest:
This one lets us define unrestricted traversals:
We do want to have
traverseOfU
otherwise we have to define twotraversals for every data structure: one unrestricted and one not. And
they are really the same. Which would be quite a shame.
KleisliU f
is\p. (Strong (,) () p, Strong Either Void p, Monoidal (,) () p)
, but I don't believe that it isWandering
or, if it is,it doesn't admit a trivial implementation.
So if we have traversals defined in terms of
(Strong (,) () p, Strong Either Void p, Monoidal (,) () p)
they can be equally well used in alinear and unrestricted context. In fact, we may even have,
eventually, a linearity-polymorphic
Kleisli
, and get a polymorphictraversal out as a mere cast. This is very much not the case with
Wandering
. This is the reasoning behind #79.But if don't have
Wandering
how do you build a traversal? Making onemanually by composing profunctor arrows is pretty much out of the
question: it is very cumbersome and allocate a ton as you are forced
to decompose your type into a sequence of
Either
and binary(,)
since it's the only language that the profunctor speaks.
There is a generic way to make one from a Van Laarhoven traversal. It
uses a special applicative to reify the traversal.
The simplest presentation of this type is
It's an interesting exercise to prove that it is indeed an
applicative. Important functions are
With this material, we have:
It is then sufficient to know how to traverse
Batch
with aprofunctor, which can be done once and for all.
That being said, we still have to allocate a lot to do a
traversal. And this extra allocation can't be removed by
specialisation, since traversals are usually recursive.
It does seem at this point in my thought process that we have two
definitions: one is good for writing new traversals, the other one is
good for using traversals. That's bad! And I don't quite know what the
best solution is yet.
Appendix: A possibly more efficient
Batch
If you have done the exercise above (I'm watching you!), you will have
realised that there are a lot of lists concatenation in this
story. List concatenations are bad.
But, before I propose a way to avoid them let's first make things
worse. Because another potential issue with
Batch
is the presence ofa partial function throughout. It's not really a problem for a type
used only internally, but, at any rate, it can be eliminated. I'll
give the definition that was actually used in #79
It's structured as a list of
a
terminated by a functionb %1 -> … %1 -> t
with the appropriate arity.There is no partiality here. But everything is horribly slow: even the
Functor
instance requires a recursion.By the way, it's some kind of free applicative structure. We can find
the same type in this sweet blog post about sorting
Traversable
s.At the very least, if we want to reify the traversal through some
applicative functor, none of the functions of interest should be
recursive. So we kind of want to have concatenation built in. Here is
my attempt
Honestly though, it's not enough to convince me. I want to read
traversals as some kind of iterator in Rust, or generator in Python,
etc… But here, we still need to reify the recursive structure. So,
basically, a structure which would otherwise be only on the stack is
now duplicated in the heap. It prevents many optimisation, including
inlining with non-recursive traversals, so I'm really not satisfied.
Bonus thoughts on Traversable-by-data
While I'm at it, let's speak about traversal but with
Data.Applicative
instead. See also #190.Basically, in the scope of the Optics library, these are very special
citizen: they don't really compose with anything. A lens composed with
a traversal-by-data is a regular traversal (by control). Same with a
prism. So to be traversable by data you basically need to be a
composition of traversable-by-data.
We will have, just as is the case for the normal traversal, two
definition.
Notice the absence of
Strong
: traversals-by-data don't compose withmuch. I don't think we can avoid
Monoidal Either Void
here, so thatwould be an argument to add
Monoidal Either Void
to the constraintsin the regular traversal case if we were to go this way: for
subtyping.
I don't think we need these for the first release, really: they are,
indeed, pretty special. But we may want them eventually
nonetheless. So these were my thoughts on them.
The text was updated successfully, but these errors were encountered: