On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel < rendel@mathematik.uni-marburg.de> wrote:
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/... the assocative laws from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... The definitions of Braided and Symmetric from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/html/... and the Monoidal class from: http://hackage.haskell.org/packages/archive/category-extras/0.52.1/doc/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/... let alone a CCC http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/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/... 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