Handle common parameter orderings.

[sellout]

Given a function like

fmap :: (a -> b) -> f a -> f b

“reversing the arrows” strictly would give us something like:

cofmap :: f b -> f a -> (b -> a)

but we know fmap is its own dual, and that is clearly not right. If we changed the parameters to fmap like

fmap :: f a -> (a -> b) -> f b

then the dual is nicely

fmap :: f b -> (b -> a) -> f a

but we don’t want to reorder the parameters. So, perhaps a flag when dualizing functions that indicates either a full reversal (like above, which is useful in cases like >>= → =>>) or a final-parameter reversal, which would work by just swapping the order of the last arrow.

fmap :: (a -> b) -> f a -> f b
fmap :: (b -> a) -> f b -> f a
--                 |__________|

Alternatively, we could pass an index to indicate which parameter should be swapped with the result – but I’m not aware of any cases off the top of my head that wouldn’t dualize properly on either the first or last parameter (please add examples if you know of any).

[rocketnia]

I think I could use some help understanding how reversing the arrows works. Using a simple swap of the direction of each ->, I get much different answers than your examples...

fmap :: (a -> b) -> (f a -> f b)
cofmap :: (f b -> f a) -> (b -> a)

fmap :: f a -> ((a -> b) -> f b)
cofmap :: (f b -> (b -> a)) -> f a

I think this is the closest I come to being able to explain why Functor should be the dual of itself:

Say we're working in a set theory Meta as we formalize small categories. Let the function f : Obj(C) ->[Meta] Obj(D) be the object map of a functor between small categories C and D, and let fmap be the arrow map of the same functor. Then the signature of fmap doesn't change if we flip the small categories:

fmap :: (a ->[C] b) ->[Meta] (f a ->[D] f b)
cofmap :: (a <-[C] b) ->[Meta] (f a <-[D] f b)

We leave Meta unflipped.

I'm not sure how to have a library detect or be configured for certain arrows to remain unflipped like this. I'm also not sure I'm on the right track with my understanding. Nevertheless, I hope this comment helps you or gives someone the opportunity to help me. XD

[sellout]

I could definitely use help understanding it, too!

I have some guidelines, but I don’t think they’re at the right conceptual level. E.g., “reversing the arrows doesn’t reverse the associativity”, so

>>= :: Monad f   =>  f a -> (a -> f b)  -> f b
=>> :: Comonad f =>  f b -> (f b -> a)  -> f a -- correct
=?> :: Comonad f => (f b -> (f b -> a)) -> f a -- incorrect

I think that, ignoring currying, any function really has some number of parameters and in different languages we have different motivations for choosing an ordering of those parameters. E.g., in Haskell, we choose

fmap :: (a -> b) -> f a -> f b

to ease the most common partial application, whereas in Scala, we choose

def map[A, B](fa: F[A])(f: A => B): F[B] // fmap :: f a -> (a -> b) -> f b

to ease type inference. But in both cases, we have {f a, a -> b} -> f b, where {,} denotes something like a multiset of parameters (i.e., the order of them is irrelevant).

For a more complicated example, see https://github.com/slamdata/matryoshka/pull/69#issuecomment-282791974, which goes on for a while discussing how the parameters to {Monad m, Comonad w, Functor f} => {f w ~> w f, m f ~> f m, w f b -> b, a -> m f a, a} -> b should be ordered. Haskell would tend to use that ordering, while Scala would tend to have a first instead of last.

In this issue’s description, I called what the >>= example does “full reversal”, but I think that was probably not right. In both Haskell & Scala, when we take the dual of something like the Matryoshka example, we don’t reverse the order of all the parameters. It’s more like there is some “primary” parameter that is swapped for the result when taking the dual and all the other parameters (or, their duals anyway) stay in the same position. But I don’t know how to identify that parameter mechanically … and I don’t know how to describe this categorically.

[rocketnia]

Thanks for all that detail!

It’s more like there is some “primary” parameter that is swapped for the result when taking the dual and all the other parameters (or, their duals anyway) stay in the same position.

That sounds like the same situation where the ->[Meta] rationalization can go through. Move the primary parameter to the end, make the last parameter use a small arrow while the rest of the immediate parameters use large arrows, and then reverse only the small arrows:

(=<<) :: (Monad m) => (a ->[C] m b) ->[Meta] (m a ->[C] m b)
  -- where we pick the category C so that m is a functor from C to C

(<<=) :: (Comonad w) => (a <-[C] w b) ->[Meta] (w a <-[C] w b)
  -- where we pick the category C so that w is a functor from C to C

A more category-theoretical notation would be something like (=<<) :: Hom(a, m b) -> Hom(m a, m b), and a more type-theoretical or proof-theoretical notation would be the sequent (Gamma |- f : a -> m b) --- (Gamma |- ((=<<) f) : m a -> m b). Then what I'm calling "large arrows" are respectively set-theoretical functions or sequents, and "small arrows" are respectively hom-sets or function types/logical implications.

Higher-order languages make it easy to collapse the metatheory and commute (x ->[Meta] (y ->[C] z)) to make (y ->[???] (x ->[???] z)). I suspect this is why it would be necessary to track down a "primary" parameter again to take a categorical dual.

I think occurrences of ->[Meta] aren't the only "large arrows" at play here. If we just look at Monad and Comonad, there seem to be some other large arrows that keep pointing the same way:

• Universal quantification of type variables doesn't become existential quantification.
• Implementations of Monad must implement both return and (>>=). For Comonad, this requirement doesn't flip around to become an "implement whichever method you want" requirement.

I think a lot of my trouble understanding unfamiliar duals, which particularly trips me up when it comes to understanding coinduction, is that I form some intuitive understanding of the original thing based on a higher-order interface, and then I don't know which arrows of that interface are being flipped this time and which aren't.

Anyway, it seems like if there's a good design for this flag you're talking about, it's probably close to what you've described. Like... I start to wonder what kind of DSL would let people pick out exactly which arrows to reverse and which arrows not to, but I bet in most cases people are probably going to write their type class definitions according to a small number of conventions that can be directly supported by this tool.

[rocketnia]

Hmm, I suppose category theory notation is especially apt here, not just because of this being the categorical dual we're talking about, but because Hom(...) doesn't usually nest. If we have exponential objects, that gives us a notation that can finally nest, which I'd have to call "smaller-still arrows" or something. :-p

Hm. Not to design your library for you, but I wonder if it would be easier to cut code in half by having a syntax to define both one thing and its dual at the same time. That way this syntax could be explicit about which arrows are set-theoretical functions (for the purposes of this dual), which arrows are hom-sets, and which arrows are exponentials.

But... I think I'm very confused and couldn't actually follow through on this approach if I tried. XD; Sorry, just idle thoughts I guess.

[sellout]

I like the Hom explanation. That is more obvious in literal code when dealing with polykinded (or at least higher-order) functors:

fmap :: PFunctor f => (a ~> b) -> (f a ~> f b)

and yes, with =<< (not >>=). Of course, since this is actual code, I still have to solve it for >>= and other “flipped” functions … but at least it clarifies what’s happening under the hood.

Thanks, that was very edifying.

Re: defining the thing and its dual simultaneously – Seems cool. I think I’ll explore that, but I will still also need to add mappings for stuff defined in base and other libraries (for compatibility), so I still need to get this other aspect working.