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.

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.