Traversable and zippers. Necessity and sufficiency

Question

Every type T overloading the Traversable brings forth a Zipper T. I.e. existence of the instance Traversable T is the sufficient condition of the Zipper T.

Is there a proof that this is also a necessary condition? (I suppose it must be pretty trivial, but I didn't found formal general definition of the zipper so far.)

Inwards

Answer 1

Every Traversable functor is a container with finitely many positions for elements. In order to combine the effects for computations at each element, there must only be finitely many. So, for example, the infinite Stream functor is not Traversable, because there is no way to deliver a reliable function which pulls Maybe through. We'd need

sequence :: Stream (Maybe x) -> Maybe (Stream x)

but if you want to check that everything in the stream succeeds, you'll have a long wait.

Zippers correspond to the ability to identify a particular element position (which further gives rise to a connection with derivatives, but that's another story). To be able to plug an element back in its hole, you need an effective way to decide equality on positions. If you have only finitely many positions, that's bound to be true (in the absence of information-hiding). So being Traversable is certainly sufficient for having a Zipper.

It's not necessary, however. Stream has a perfectly sensible Zipper

type StreamContext x = ([x], Stream x)
type StreamZipper x = (StreamContext x, x)

which represents the context as a finite (ok, ok, add a bang or two) list before the selected element and an infinite stream after it.

The positions in an infinite Stream are natural numbers. Natural numbers have a decidable equality, but there are infintely many of them.

tl;dr finite implies countable, but not vice versa.

Stalinism

This doesn't sound quite right. It's perfectly OK to sequence an infinite list of IO actions, for example. (Say sequence $ map print $ [1..]) – Cauline

IO is not a very helpful example of a monad, because it just keeps on rocking in the real world. Sequencing over a stream is thus ok. But what's true of IO is not indicative of monads in general. You cannot compute if an infinite sequence of Maybes are all Just. – Stalinism

It's nothing special to do with IO. It works with any Applicative that is sufficiently lazy. Another example: snd $ runWriter $ sequence_ $ map (tell . return) $ [1..] :: [Int]. You are correct about Maybe, but still there are plenty of cases where it makes sense to sequence an infinite container. – Cauline

You speak in favour of dishonesty. By all means consider what it means to be a "sufficiently lazy" Applicative. But Traversable promises to work with every Applicative. So you're right that there's something else to think about. But you're wrong on this point of fact. – Stalinism

Sorry, I didn't mean to offend you. And in any case, I'm not sure where we disagree. – Cauline

I'm not offended. But I am in favour of accuracy. In the case of lists, sequence works if the lists are finite (as we often pretend they must be) or the computations are sufficiently lazy. In the case of explicitly infinite streams, it seems perverse to offer to traverse with effects whether lazy or strict. The gap between the two is interesting: for infinite structures with lazy effects, we get only an approximation to a "run" function. Where we disagree is that I don't think happening-to-work-by-luck-not-typechecking makes something perfectly OK. – Stalinism

@pigworker: do you think a Traversable instance should be provided for lists? I could equally say "it seems perverse to offer to traverse with effects whether finite or infinite." If you can pretend lists are finite, why can't I pretend the Applicative is sufficiently lazy? Regardless, this area is one in which the current Haskell type ecosystem is too coarse a tool to provide much assistance, and I think we'd both appreciate something a bit more refined. – Afrika

Indeed I'm unhappy with the "but we really mean finite lists here" remaining an informal external remark, rather than a type-managed property, but that ship sailed a long time ago. In Agda, I'm happy to distinguish lists from colists and have only the former Traversable. The Applicative/Traversable setup is young enough that we could maybe go to the trouble of thinking this through. Especially if we can sort out DefaultSuperclassInstances. – Stalinism