Traversable: A Remix

[duplode]

Comment thread for Traversable: A Remix.

[ncfavier]

Are you defining a category whose objects are the objects of Hask, and whose morphisms a ⇝ b are pairs of an applicative functor f and a morphism a → f b, in other words exists f. Applicative f *> a -> f b? Because if so, Traversable does not correspond to an endofunctor on this category, because traverse is not allowed to change the functor.

If it was, you could make any functor Traversable by always picking the return functor to be Const ().

[duplode]

@ncfavier It's largely like that, but f is not existentially quantified. While it's tempting to use existential quantification to make the types line up with the usual class hierarchies, doing that would stop us from actually using any f b results (as that requires knowing what f is). Without existential quantification, there are no qualms in having traverse keep the same f, as it must.

[ncfavier]

What are the morphisms, then? f has to come from somewhere

If you fix an f and say the morphisms are a → f b, that's not a category unless f is a monad.

I get the intention, but I don't think it really works as a categorical formalisation of traversables. AFAIK it's much easier to go via sequenceA: a Traversable is a Functor that distributes over every Applicative.

[duplode]

The morphisms between a and b are functions a -> f b for all choices of applicative f. As far as setting up the category goes, we don't need to keep f fixed: it suffices for composition, (<%<), to combine the effects in a way that's associative and unitary.

(One thing this category lacks when compared to the Kleisli category we get from Monad is an analogue of (=<<) :: Monad a => (a -> m b) -> m a -> m b, which is the morphism mapping of a functor to Hask. That, though, doesn't stop us from defining the category itself.)

[ncfavier]

functions a -> f b for all choices of applicative f

I don't understand what you mean by this, formally. If it's not existential quantification, is it universal quantification (forall f. Applicative f ⇒ a → f b)? I guess then pure could be your identity, but how do you define composition ((∀ f. Applicative f ⇒ a → f b) → (∀ f. Applicative f ⇒ b → f c) → (∀ f. Applicative f ⇒ a → f c))?

(This also still doesn't match the type of traverse.)

[duplode]

I don't understand what you mean by this, formally. If it's not existential quantification, is it universal quantification

There is no quantification in the types of the morphisms. Each morphism carries its own f, and composition combines them through functor composition. For instance:

foo :: Integer -> [Integer]
foo x = [-x, x]

bar :: Integer -> Maybe Integer
bar x = if x < 0 then Nothing else Just x

(<%<) :: (Applicative f, Applicative g) =>
    (b -> g c) -> (a -> f b) -> (a -> Compose f g c)
g <%< f = Compose . fmap g . f

foo and bar are both morphisms from Integer to Integer, and so is their composite bar <%< foo, even though they carry different sorts of effects.

[ncfavier]

There is no quantification in the types of the morphisms. Each morphism carries its own f

Then where is the quantification? f has to be bound somewhere, otherwise it is undefined. The common mathematical meaning of "each morphism carries its own f" is that morphisms are dependent pairs of a functor f and a function a → f b, which is another way of saying existential quantification. And I do think this is what you had in mind, but it doesn't work, for the reasons I've already said: if traverse h is a morphism in this category, then it also "carries its own f", but this doesn't match the actual type of traverse, where the f in the result is the same f you passed in (through h).

If you're still not convinced, I urge you to try and define this category using a formalisation library like 1lab.

To be clear, the claims in your blog post are currently either wrong or not sufficiently well-explained. They might be salvageable, but I don't yet know how (perhaps there is some hope of taking the Kleisli category of the free monad associated with f, or something).

[duplode]

I believe the points each of us are making are about different things, and they don't contradict each other. If I understand your objection correctly, you're noting that we can't have a type inhabited by all morphisms from a to b without existentially quantifying the applicative functor or, perhaps, restricting the choice of applicative and reworking things in terms of some free monad. While that's indeed the case, my point is that the category can nonetheless be defined even in the absence of such a type (and, accordingly, I haven't attempted to define said type anywhere), though that formulation also has its limitations (in particular, it costs us the ability to work with the morphisms in a first-class way, through objects in Hask of their own).

[ncfavier]

In order to define a category, you have to say what its objects are (in this case, types) and what its sets (or types, I'm not picky about foundations) of morphisms $Hom(a, b)$ are. While there are legitimate concerns about whether this can really be done formally when talking about a language like Haskell, this is not my point. We can talk about the category of sets if you like.

My point is that you have not defined what the Hom-sets of this category are at all, and so you have not defined a category in any meaningful sense; and, furthermore, I claim that you cannot do so in a way that satisfies the claims in your post, at least without drastically redefining the meaning of "category" and/or "endofunctor".

Taking our foundations to be dependent type theory, here are some examples of things that would make sense to use as Hom types, in pseudo-Agda:

• λ a b → a → f b, for some f : Type → Type in the context
• λ a b → Σ (Type → Type) (λ f → Applicative f × (a → f b)) (existential quantification)
• λ a b → (f : Type → Type) → Applicative f → a → f b (universal quantification)

[duplode]

To bring some closure to this discussion: firstly, the divergence about existentials doesn't really go beyond terminology, as I was talking of "weak" existentials as featured in Haskell; there's no issue if we're dealing with sigma types.

Secondly, a little exploration with agda-categories suggests a workable encoding could be made along the following lines (using a plain endofunctor instead of applicative, which is good enough for illustrative purposes):

TrCat : Category (suc 0ℓ) (suc 0ℓ) (suc 0ℓ)
Category.Obj TrCat = Set₀
Category._⇒_ TrCat = λ A B → Σ (Endofunctor (Sets 0ℓ)) (λ F → A → Functor.₀ F B)

TrCat is one level above the base universe of types. While that's clearly not as good as having it in the same universe, I believe that doesn't make the definition meaningless.

While I'd like to have offered a full proof of concept, I don't actually know Agda yet: a little more fluency is needed for me to produce something presentable, and I couldn't get back to this since August. I'll wrap it up eventually, though.

[ncfavier]

In that case, my first comment still holds (but maybe I wasn't very clear): while it is true that every traversable endofunctor yields an endofunctor on TrCat (assuming you add the requisite Applicative structure), the converse direction does not hold: an endofunctor on TrCat does not necessarily give rise to a traversable functor.

In fact, every type constructor/family Set → Set (not even necessarily functorial) gives rise to an endofunctor on TrCat, simply by picking Const 1 as the return functor always. Compare:

traverse :: ∀ f. (a → f b) → (t a → f (t b))
fmapTrCat :: (∃ f. a → f b) → (∃ g. t a → g (t b))
          :: ∀ f. (a → f b) → ∃ g. t a → g (t b)

[duplode]

Indeed: while, as the post states, traverse is the arrow mapping of an endofunctor of TrCat, the functor laws alone do not ensure the mapping will be a lawful traverse. For the converse to hold, we'd at a minimum need some form of the naturality law of Traversable, which is no longer granted by parametricity.

[ncfavier]

So here's something we can do: to make things precise, let's define the category $\mathcal{T}$ (your TrCat) as follows:

• objects are sets;
• morphisms $A \to^\mathcal{T} B$ are (dependent) pairs of an applicative functor $F$ and a function $f : A \to F B$ (we say that $f$ is over $F$, for reasons that will hopefully get clear later);
• identity morphisms are given by identities in Set over the identity functor $A \to \rm{Id}\ A$;
• the composition of $f : B \to F C$ and $g : A \to G B$ is $Gf \circ g$ over $G \circ F$ (note the opposite order).

We can also consider the restriction $\mathcal{A}$ of the category of categories to the single object Sets and the applicative functors (explicitly, this has a single object $*$, and morphisms $* \to *$ are applicative functors on Sets, with the usual identity and composition of functors).

There is a projection functor $p : \mathcal{T} \to \mathcal{A}^\rm{op}$ that sends every set to $*$ and sends a morphism $f : A \to F B$ over $F$ to the applicative functor $F$. The identity law for $p$ says that the identity morphisms in $\mathcal{T}$ are over the identity functor, while the composition law says that the composite is over the composite functor, which is how we've defined $\mathcal{T}$.

Finally, we can define a traversable functor as an endofunctor $T : \mathcal{T} \to \mathcal{T}$ that respects the projection, in the sense that $p \circ T = p$. This condition expresses that $T$ leaves the underlying applicative functor unchanged: it takes $f : A \to FB$ to $Tf: TA \to FTB$.

Another (equivalent) perspective on this is via displayed category theory (nlab, 1lab): the projection $p$ is really meant to suggest that $\mathcal{T}$ is a category displayed over $\mathcal{A}^\rm{op}$: the objects over the point are sets, and the morphisms over $F$ are exactly what I've been calling morphisms over $F$. Then a traversable functor should correspond to a vertical endofunctor (1lab) on $\mathcal{T}$ (if you squint, you can see how ∀ {f} → 𝒯.Hom[ f ] a' b' → 𝒯.Hom[ f ] (F₀' a') (F₀' b') looks like a traversal once you inline the relevant definitions).

---

As a technical aside, in addition to the "size issues" you noticed (having to raise the universe level), there is also a "homotopy size" issue: from the perspective of homotopy type theory / univalent foundations, there is not really a set of endofunctors on Sets, but rather a groupoid of them (because there is in general more than one way two endofunctors can be isomorphic), so $\mathcal{A}$ really "wants" to be a bicategory rather than a category, and so you'd end up with some sort of displayed bicategory and I have no idea how those work. But for Haskell it's fine to just assume that we're doing set-level mathematics, as one rarely cares about identifying functors up to isomorphism for programming.

I think the full 2-categorical construction of $\mathcal{T}$ would embed into the "universal Cat-cobundle/colax slice" (nlab) (just looking at the connected component of Sets and the lax monoidal functors), so it would be quite natural from a theoretical perspective, but now I'm using words I barely understand.

Sorry for infodumping. I should get my own blog lol

[ncfavier]

Found some related work by @Lysxia using "graded endofunctors" instead of vertical endofunctors (but they seem like completely equivalent notions) https://gist.github.com/Lysxia/c400ccee1e1c437e37682f39df2f6946