Would a type class "between" Category and Arrow make sense?

Question

Often you have something like an Applicative without pure, or something like a Monad, but without return. The semigroupoid package covers these cases with Apply and Bind. Now I'm in a similar situation concerning Arrow, where I can't define a meaningful arr function, but I think the other functions would make perfect sense.

I defined a type that holds a function and it's reverse function:

import Control.Category

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

reverse (Rev f g) = Rev g f
apply (Rev f _) x = f x
applyReverse (Rev _ g) y = g y
compose (Rev f f') (Rev g g') = Rev ((Prelude..) f g) ((Prelude..) g' f') 

instance Category Rev where
  id = Rev Prelude.id Prelude.id
  (.) x y = compose x y 

Now I can't implement Arrow, but something weaker:

--"Ow" is an "Arrow" without "arr"
class Category a => Ow a where
  first :: a b c -> a (b,d) (c,d)
  first f = stars f Control.Category.id

  second :: a b c -> a (d,b) (d,c)
  second f = stars Control.Category.id f

  --same as (***)
  stars :: a b c -> a b' c' -> a (b,b') (c,c')

 ...
 import Control.Arrow 

 instance Ow Rev where
    stars (Rev f f') (Rev g g') = Rev (f *** g) (f' *** g')  

I think I can't implement the equivalent of &&&, as it is defined as f &&& g = arr (\b -> (b,b)) >>> f *** g, and (\b -> (b,b)) isn't reversable. Still, do you think this weaker type class could be useful? Does it even make sense from a theoretical point of view?

Novocaine

Aren't Arrow functions exactly the definition of a category ? – Emotion

No, the Category functions are the definition of a category. Well, morphisms, anyway (and no laws)—as I understand it, Category corresponds to a subcategory of Hask which has the same objects (all types) but different morphisms. Arrow adds a lot more structure, but I don't know enough to say anything about what sort of structure. – Nadabb

@Antal S-Z: Not a subcategory, actually. Category specifies a category whose objects are those of Hask with arrows given by some 2-ary type constructor. Functor describes a subcategory of Hask whose arrows are those of Hask with objects given by some 1-ary type constructor. Applicative maps the monoidal structure of (,) to the Functor, while (&&&) etc. map it to the Category. And arr gives a functor from Hask to the Category. – Ukulele

@Antal S-Z: Also, ArrowApply makes the Category cartesian closed, giving the full power of lambda calculus with higher-order arrows, currying, etc., and the ability to map all of that from Hask to the Category. Arrows from a fixed object then give the usual Reader monad structure, which is why Kleisli m a b is isomorphic to ReaderT a m b. – Ukulele

@C.A.: Thanks, makes sense. I'm studying CS, but I'm still only a dabbler in CT (if that). Hopefully that'll change. – Nadabb

@Antal S-Z: I'm no more than a dabbler myself, just enough to translate major concepts between mathematical descriptions and Haskell implementations. Alas, I'm still badly confused by higher-level generalizations and properties of categories that don't resemble Haskell, since all my intuition-building comes from the programming side. – Ukulele

@C.A.McCann I know this is an old question, but I just found it while googling. ArrowApply does not make the category cartesian closed as the axioms of Arrows don't make tuples products. – Drusilla

@Anonymous: You are quite correct. If memory serves me, quite a few specific Arrow instances indeed fail to have products. – Ukulele

Answer 1

This approach was explored in "There and Back Again: Arrows for invertible programming": http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.9383

For precisely the reasons you're running into, this turned out to be a bad approach that wasn't picked up more widely. More recently, Tillmann Rendel produced a delightful approach to invertible syntax that substituted partial isomorphisms for biarrows ( http://www.informatik.uni-marburg.de/~rendel/rendel10invertible.pdf ) . This has been packaged up on hackage for folks to use and play with: http://hackage.haskell.org/package/invertible-syntax

That said, I think an arrow without arr makes a certain amount of sense. I just don't think that such a thing is an appropriate vehicle to capture invertible functions.

Edit: There's also Adam Megacz's Generalized Arrows (http://www.cs.berkeley.edu/~megacz/garrows/). These are maybe not useful for invertible programming either (though the basic typeclass does seem to be inveritble), but they do have uses in other situations where arr is too strong, but other arrow operations may make sense.

Erechtheum

Answer 2

From a Category Theory standpoint, the Category type class describes any category whose arrows can be describedn straightforwardly in Haskell by a type constructor. Almost any additional feature you want to build on top of this, in the form of new primitive arrows or arrow-building functions, will make sense to some extent if you can implement it using total functions. The only caveat is that adding expressive power can break other requirements, as often happens with arr.

Your specific example of invertible functions describes a category where all arrows are isomorphisms. In a shocking twist of the completely and utterly expected, Edward Kmett already has an implementation of this on Hackage.

The arr function roughly amounts to a functor (in the category theory sense) from Haskell functions to the Arrow instance, leaving objects the same (i.e., the type parameters). Simply removing arr from Arrow gives you... something else, which is probably not very useful on its own, without at least adding the equivalents of arr fst and arr snd as primitives.

I believe that adding primitives for fst and snd, along with (&&&) to build a new arrow from two inputs, should give you a category with products, which is absolutely sensible from a theoretical point of view, as well as not being compatible with the invertible arrows you're using for the reasons you've found.

Ukulele

There's no principled way to write &&& for Rev (or Iso, if you prefer). Why, you ask? Because b -> a and c -> a don't give you any way to get (b,c) -> a such that your a -> b and a -> c are both guaranteed to give back your orig b and c. – Erechtheum

Similarly, you can't write a proper fst and snd for Iso either! What's the inverse of (a,b) -> a? This is really why you need partial isomorphisms. (You can of course write a first, and second however, fwiw). – Erechtheum

@sclv: Yep. In fact, both (***) and (+++) should be fine, as well as functions giving the associative, commutative, and distributive properties of the product/sum types. But (&&&) and (|||) can't work in the general case. – Ukulele

Oops -- misread your post at first. We're in violent agreement :-) – Erechtheum

No worries. It's a helpful clarification of why anything resembling the categorical product can't work. The arrows have to preserve information, probably giving some something like linear logic instead of the intuitionistic logic we're used to. – Ukulele