mroman42 / vitrea

Optics via the profunctor representation theorem
GNU General Public License v3.0
23 stars 3 forks source link

Do Folds without functoriality exist? #4

Open considerate opened 2 years ago

considerate commented 2 years ago

In the paper, def. 3.34. folds are described as optics for the action of foldable functors. However, there is no Functor superclass constraint on Foldable in Haskell.

Unfortunately, while it seems that we can define a category for Foldables, the monoidal category seems to require the functoriality of the objects because otherwise the bifunctor Compose and the bifunctor App cannot be implemented (it might be possible using coercions but I don't know if that forms a proper functor). EDIT: it is not possible to implement either of the bifunctors, even with coercions.

Is there a way to define folds as optics without reaching for functors?

mroman42 commented 2 years ago

Let me rephrase to see if I am understanding correctly. Consider the category of set assignments, or endofunctors on the discrete category of Sets. An object in this category is a function assigning a set X to a set F(X). A morphism F -> G is a transformation, a family of morphisms F(X) -> G(X) that does not necessarily satisfy any naturality condition. The problem is that you would need to define a monoidal action by evaluation of these things that are not functors, so you would not have a monoidal action really.

I guess we could push the definition of optic a bit to get what you want, but I am not sure I understand what was your motivation. What are examples of foldable that are not functors that you would like to capture?

considerate commented 2 years ago

What are examples of foldable that are not functors that you would like to capture?

One of the more canonical examples in Haskell would be Set which is Foldable but not Functor due to its Ord constraint for Set.map which isn't required to fold over the set. It might be possible to define folds over Set if you somehow add to the constraint of the category you're working in to have all objects of the functors to be Ord but then you don't get folds over both sets and unordable lists.

The problem is that you would need to define a monoidal action by evaluation of these things that are not functors, so you would not have a monoidal action really.

Yeah, that was my reasoning as well but I really like the theory presented in the paper and feel like it would be nice if the representation could extend to folds that are isomorphic to folds in e.g. the van Laarhoven encoding or the profunctor optics in optics-core.

The constraints on the profunctor in optics-core are given by:

Constraints A_Fold             p = (Bicontravariant p, Cochoice p, Traversing p)
mroman42 commented 2 years ago

Thank you for taking the time to detail the issue.

1) I see. So we could still have a functor from the category of Ord's, but now we would have two 'folds', one for ordered things and another one for unordered things. Perhaps we could still map one to the other, but I could try to see if there is a better solution (at least for the code). 2) Oh, I did not know about this representation using Bicontravariant, Cochoice, Traversing. Does it reduce somehow to the Folding one? I would like to see if we can find a Yoneda derivation for that one.

considerate commented 2 years ago

Please excuse the brevity of my reply:

Does it reduce somehow to the Folding one?

This function is one of the functions that witnesses the reduction to a list fold.

considerate commented 2 years ago

I took a look at the the folds from a different perspective and was able to define this:

newtype Folding a b s t = Folding {getFold :: forall m. Monoid m => (a -> m) -> (s -> m)}

newtype Tagged t a = Tagged a

instance (Category obd d) => Profunctor Any (->) obd d (Folding a b) where
  dimap l _ (Folding f) = Folding $ \am x -> f am (l x)

instance Bifunctor Any (->) Any (->) Any (->) Tagged where
  bimap _ g (Tagged a) = Tagged (g a)

instance MonoidalAction Any (->) (,) () Any (->) Tagged where
  unitor (Tagged x) = x
  unitorinv = Tagged
  multiplicator (Tagged (Tagged x)) = Tagged x
  multiplicatorinv (Tagged x) = Tagged (Tagged x)

instance MonoidalAction Any (->) (,) () obd d r => Tambara Any (->) obd d Any (->) (,) () Tagged r (Folding a b) where
  tambara (Folding f) = Folding $ \am (Tagged x) -> f am x

(^..) :: s -> (Folding a b a b -> Folding a b s t) -> [a]
(^..) s l = let g = getFold (l $ Folding id) in g pure s

foldPair :: Folding a b (a,a) (b,b)
foldPair = Folding $ \f (a,a') -> f a <> f a'

foldrOf :: (Folding a b a b -> Folding a b s t) -> s -> (a -> r -> r) -> r -> r
foldrOf l s arr r = let g = getFold (l $ Folding id) in appEndo (g (Endo . arr) s) r

However, it doesn't sit right with me to encode the folding explicitly in the Monoid constraint inside Folding as opposed to figuring out what monoidal actions this would be isomorphic to. Unfortunately I haven't figured that out yet.

considerate commented 2 years ago

I found this in the optic-core package:

-- | If @p@ is a 'Profunctor' and 'Bicontravariant' then its right parameter
-- must be phantom.
rphantom :: (Profunctor p, Bicontravariant p) => p i c a -> p i c b
rphantom = rmap absurd . contrasecond absurd

This suggests to me that the reason for Bicontravariant p in the constraints for the fold is that due the contravariance and the covariance in the second argument is used to encode that the B and T objects don't appear in the equation and can thus be exchanged freely.