search

ekmett / kan-extensions

Kan extensions, Kan lifts, the Yoneda lemma, and (co)monads generated by a functor
Other
78 stars 33 forks source link

Add an Invariant version of Day #50

Closed puffnfresh closed 6 years ago

puffnfresh commented 6 years ago

Derived by combining the covariant and contravariant versions of Day. Using this as a tensor gives us a combination of Applicative and Divisible, which seems useful for things like derivation of function pairs like parsers/printers.

RyanGlScott commented 6 years ago

This seems reasonable to me on the surface. That being said, I'll let @ekmett make the call on whether to merge this, since:

  1. It adds a new dependency (invariant)
  2. I probably have a conflict of interest here, since I'm the maintainer of invariant :)
ekmett commented 6 years ago

I'm kinda meh on the request, but...

puffnfresh commented 6 years ago

@ekmett you're meh because it doesn't seem very useful?

ekmett commented 6 years ago

More because Invariant is really four classes disguised as one, so I hate enshrining it as is.

puffnfresh commented 6 years ago

@ekmett I'm not sure what four classes Invariant is disguised as. Do you know a resource which covers this?

ekmett commented 6 years ago

When you invoke xmap f g (or invmap or whatever you want to call it), the four different variants are whether you you require

1.) no laws about how f and g interact

2.) f.g = id

3.) g.f = id

4.) or both (isomorphism)

each of these 4 options describes a different category. So now we have a little diamond shaped lattice of additional superclasses sitting above Contravariant and Functor

Are you expecting users to map with arbitrary pairs of functions, split monomorphisms, split epimorphisms or isomorphisms?

Isomorphism is too strong for, say, the Fegaras-Sheard catamorphism, so then you have to consider which weakening you are going to have.

There are other options as well.

Consider that merely requiring f.g.f = f and g.f.g = g for instance allows a more adjunction-like mappings, and both are implied by either of the f.g=id or g.f=id laws. This further explodes the set of invariant-like classes that should theoretically sit above Functor and Contravariant into an even bigger lattice. Making it so you require only one or the other then weakens things further...

All of these points in the design space have different uses. All of them have different laws.

Invariant doesn't specify any requirements on the mapping at all, giving you only the first case mentioned above.

As for resource? Here you go. Here is the resource. ;)