Re: [Haskell-cafe] The Arrow class (was: Vague: Assembly line process)

Related to this, I really would like to be able to use arrow notation without "arr"; I was looking into writing a "circuit optimizer" that modified my arrow-like circuit structure, but since it's impossible to "look inside" arr, I ran into a brick wall. Has anyone done any analysis of what operations arrow notation actually requires so that they can be made methods of some typeclass, instead of defining everything in terms of "arr"? It seems to me the trickiness comes when you have patterns and complex expressions in your arrow notation, that is, you write (a,b) <- some_arrow <- (c,d) returnA -< a instead of x <- some_arrow <- y returnA -< x But I expect to be able to do the latter without requiring "arr", and that does not seem to happen. -- ryan On Wed, Jun 16, 2010 at 11:18 AM, Edward Kmett wrote:

On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel 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

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe