Connection between *WithIndex and representable functors

[Icelandjack]

Is the index of FunctorWithIndex, ... a weaker condition of representable functors?

There seems to be a strong connection

instance FunctorWithIndex r ((->) r)
type instance Rep ((->) r) = r

instance FunctorWithIndex i f => FunctorWithIndex [i] (Free f)
type instance Rep (Cofree f) = Seq (Rep f)

instance FunctorWithIndex i m => FunctorWithIndex (e, i) (ReaderT e m)
type instance Rep (ReaderT e m) = (e, Rep m)

instance (FunctorWithIndex i f, FunctorWithIndex j g) => FunctorWithIndex (Either i j) (Product f g)
type instance Rep (Product f g) = Either (Rep f) (Rep g)

instance (FunctorWithIndex i f, FunctorWithIndex j g) => FunctorWithIndex (i, j) (Compose f g)
type instance Rep (Compose f g) = (Rep f, Rep g)
...

and if so data types that only have one (FunctorWithIndex (Either i j) (Sum f g), FunctorWithIndex () Maybe) or the other (Representable Dual, Representable (Yoneda f), Representable (Day f g)) carry significance.

Not as a proposal, but would this make sense logically or are they wholly separate points in the hierarchy

class (Distributive f, FunctorWithIndex (Rep f) f) => Representable f

[ekmett]

Logically, yes, you could give them this inheritance relationship. In theory for such a role FunctorWithIndex should be a Sieve class, which is a somewhat stronger claim, and rules out some obvious FunctorWithIndex existing types, We've already made that change in the profunctors hierarchy.

There are a number of pragmatic concerns. Representable is in a package with far far fewer dependencies than lens, so moving FunctorWithIndex to make a Sieve class risks losing instances that matter or causing packaging woes.

For that matter Representable f could demand Monad f with zipping semantics and MonadFix, but we won't get those instances for Compose f g. =/

At the least I have no difficulty with making more (all?) of the representable instances into FunctorWithIndex instances.

[Icelandjack]

I'm not clear on the relationship you intend with Sieve, a class I am only familiar with in passing.

For that matter Representable f could demand Monad f with zipping semantics and MonadFix, but we won't get those instances for Compose f g. =/

So?

class (Distributive f, MonadZip f, MonadFix f) => Representable f

Losing Representable (Compose _ _) would be a loss.

At the least I have no difficulty with making more (all?) of the representable instances into FunctorWithIndex instances.

Right, (I also wonder if instances like FunctorWithIndex (Either _ _) (Sum _ _) should exist in the first place)

[ekmett]

The proper term for what we're looking for in category theory is

https://en.wikipedia.org/wiki/Sieve_(category_theory)

We're looking more properly at a Cosieve, but both sieves and cosieves are "sieves" in the general sense. The requirement that this be a subfunctor of Hom(c, _) is the hard part, because it rules out a lot of instances, repeating indices, instances that carry extra data with them, etc.

I've generally been breaking apart my representable-style classes into the sieve (index) and tabulate parts. FunctorWithIndex is a less stringent "(Co)Sieve".

[ekmett]

Sum f g isn't representable. On the other hand, it admits a perfectly good "index" to talk about the path you got to the element with. Sieving/FunctorWithIndex only needs an embedding into the "key" type, not to cover the whole thing.

It is when you go the other way with representable that the embedding needs to upgrade to isomorphism.