Typeclass for (what seems to be) a contravariant functor implementing function inversion

Question

Lets say I have the following

import Control.Category (Category, (.), id)

data Invertible a b = Invertible (a -> b) (b -> a)

instance Category Invertible where
  id = Invertible Prelude.id Prelude.id
  (Invertible f f') . (Invertible g g') = 
    Invertible (f Prelude.. g) (g' Prelude.. f')

invert (Invertible x y) = Invertible y x

Note that the following is true:

invert (g . f) == invert f . invert g

This structure seems very similar to a contravariant functor (wikipedia), as it follows the same axiom:

 F(g . f) = F(f) . F(g) 

In my case, F is simply invert.

I looked at Data.Functor.Contravariant.contramap, which has a function of the type:

(a -> b) -> f b -> f a

But I didn't know how'd I'd implement that in my situation. For example, I can't work out a sensible choice for f, and in my situation, there's no function a -> b, just invert.

However, invert nevertheless fits the mathematical axiom of a contravariant functor, so I'm thinking I can fit this into some existing class, but I just can't find which one and how to do it. Any help or pointers would be appreciated.

Hong

You might find this blog post interesting: gelisam.blogspot.com/2013/07/the-commutative-monad.html – Verve

The problem, in my humble opinion, is that invert is a contravariant endofunctor in the category of Invertible whereas Contravariant f is a contravariant endofunctor in the category of Hask. – Verve

@AaditMShah, that was my guess too, but I don't know enough category theory to be confident. – Vaulting

You may or may not already know about the lens types Iso s t a b = forall f p . (Functor f, Profunctor p) => p a (f b) -> p s (f t) and Iso' a b = Iso a a b b. Iso' ends up being isomorphic to your type. This doesn't relate to your question; I just thought you might find it interesting. – Vaulting

Answer 1

A category has two collections: objects and morphisms.

The usual Haskell prelude, and it appears that the classes in Data.Functor.Contravariant, only operate on a very narrow category, that is the category where types are objects and functions are morphisms, usually denoted Hask. The standard Functor class is also very narrow: they only represent endofunctors on Hask: they must take types to types and functions to functions.

Take for example the functor Maybe. The way Maybe acts on types is just that it takes types a to Maybe a. Maybe maps Int to Maybe Int and so on (I know this sounds a bit trivial). What it does to morphisms is encoded by fmap: fmap takes f :: (a -> b), a morphism between two objects in Hask, and maps it to fmap f :: (Maybe a -> Maybe b), another morphism in Hask between the objects that the functor maps to. In Haskell we could not define a Functor which takes e.g. Int to Char -- all Haskell Functors have to be type constructors -- but in general category theory we could.

Control.Category generalizes a little bit: the objects of a Control.Category category C are still types[1] just like in Hask, but its morphisms are things of type C a b. So in your example, the objects are still arbitrary types, but your morphisms are things of type Invertible a b. Since your morphisms are not functions, you will not be able to use the standard Functor classes.

However, it's a fun exercise in building up your category theory knowhow to define a functor class which operates between Category categories rather than assuming Hask, which would capture your example. Remember, a functor acts on objects (types) and morphisms.

I'll leave you with that -- feel free to comment if you would like more guidance.

---

[1] Ignoring PolyKinds, which makes this a bit more general.

Illustration

You beat me to it. I knew that the problem was because the OP was trying to marry Prelude.id with Control.Category.id and Prelude.. with Control.Category.., but I didn't get the time to write an answer. I was led astray by the following blog post: gelisam.blogspot.com/2013/07/the-commutative-monad.html – Verve

Lets say we reverse what's found in Control.Categorical.fmap which is r a b -> t (f a) (f b). Instead reverse to be contramap :: r a b -> t (f b) (f a). Let r = Invertible and t = Invertible. From here we've got contramap :: Invertible a b -> Invertible (f b) (f a). I guess at this point we just need "f" to be Id? – Hong

@Hong Indeed. You would define class (Category c, Category d) => Contravariant f c d | f c -> d, f d -> c where contramap :: c x y -> d (f y) (f x). Then you would define instance Contravariant Identity Invertible Invertible where contramap (Invertible f g) = Invertible (Identity . g . runIdentity) (Identity . f . runIdentity). Now you have contramap isomorphic to invert. However, I doubt that you would want to use contramap because you would have to deal with an unnecessary Identity wrapper. You're better off simply using the invert function directly. – Verve