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

[Edward Kmett]

On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel <
rendel at 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/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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100616/b5309b53/attachment.html