Bas van Dijk wrote:

data Iso (⇝) a b = Iso { ab ∷ a ⇝ b
, ba ∷ b ⇝ a
}

type IsoFunc = Iso (→)

instance Category (⇝) ⇒ Category (Iso (⇝)) where
id = Iso id id
Iso bc cb . Iso ab ba = Iso (bc . ab) (ba . cb)

An 'Iso (⇝)' also _almost_ forms an Arrow (if (⇝) forms an Arrow):

instance Arrow (⇝) ⇒ Arrow (Iso (⇝)) where
arr f = Iso (arr f) undefined

first (Iso ab ba) = Iso (first ab) (first ba)
second (Iso ab ba) = Iso (second ab) (second ba)
Iso ab ba *** Iso cd dc = Iso (ab *** cd) (ba *** dc)
Iso ab ba &&& Iso ac ca = Iso (ab &&& ac) (ba . arr fst)
-- or: (ca . arr snd)

But note the unfortunate 'undefined' in the definition of 'arr'.

This comes up every couple of years, I think the first attempt at formulating Iso wrongly as an arrow was in the "There and Back Again" paper.

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.60.7278

It comes up now and again, because the types seem to _almost_ fit. =) The reason is that an arrow is a closed pre-Cartesian category with a little bit of extra structure. Isomorphisms and embedding-projection pairs are a bit too constrained to meet even the requirements of a pre-Cartesian category, however.

This seems to suggest that all the methods besides 'arr' need to move
to a separate type class.

You may be interesting in following the construction of a more formal set of categories that build up the functionality of arrow incrementally in category-extras. An arrow can be viewed as a closed pre-cartesian category with an embedding of Hask. Iso on the other hand is much weaker. The category is isomorphisms, or slightly weaker, the category of embedding-projection pairs doesn't have all the properties you might expect at first glance.

You an define it as a Symmetric Monoidal category over (,) using a Bifunctor for (,) over Iso:

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html

the assocative laws from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/Control-Category-Associative.html

The definitions of Braided and Symmetric from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/Control-Category-Braided.html

and the Monoidal class from:

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/Control-Category-Monoidal.html

This gives you a weak product-like construction. But as you noted, fst and snd cannot be defined, so you cannot define Cartesian

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Category-Cartesian.html

let alone a CCC

http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Category-Cartesian-Closed.html

or Arrow. =(

Wouldn't it be better to have a definition like this:

class Category (~>) => Products (~>) where
(***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d))
(&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c))
fst :: (a, b) ~> a
snd :: (a, b) ~> b

You've stumbled across the concept of a Cartesian category (or at least, technically 'pre-Cartesian', though the type of product also needs to be a parameter or the dual of a category with sums won't be a category with products.

http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/Control-Category-Cartesian.html

Or even like this:

class Category (~>) => Products (~>) where
type Product a b
(***) :: (a ~> b) -> (c ~> d) -> (Product a c ~> Product b d)
(&&&) :: (a ~> b) -> (a ~> c) -> (a ~> Product b c)
fst :: Product a b ~> a
snd :: Product a b ~> b

This was the formulation I had originally used in category-extras for categories. I swapped to MPTCs due to implementation defects in type families at the time, and intend to swap back at some point in the future.

Unfortunately, I don't see how to define fst and snd for the Iso example, so I wonder whether Iso has products?

It does not. =)

-Edward Kmett