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

[Tillmann Rendel]

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 seems to suggest that all the methods besides 'arr' need to move
> to a separate type class.

I agree. The power of Arrows as they currently are is that we can 
enlarge the ordinary set of functions (->). But if arr would be excluded 
from the Arrow class, we could remove arrows, too. For example, in your 
Iso example, we want to consider not all morphisms, but only the 
isomorphisms.

It would be nice to have a standard type class to express this kind of 
thing, and it would be nice to have arrow notation (or some variant of 
arrow notation) for it.


However, I'm not so sure about the types of (***) etc. Currently, we have

   (***) :: (a ~> b) -> (c ~> d) -> ((a, c) ~> (b, d))
   (&&&) :: (a ~> b) -> (a ~> c) -> (a ~> (b, c))

This seems to say that (~>) has products as follows: The object part of 
the product bifunctor is (,), the morphism part of the product bifunctor 
is (***), the mediating arrow is constructed by (&&&), and the 
projections are (arr fst) and (arr snd).

I see two problems with this definition: The object part of the 
bifunctor is fixed, and the projections are given in terms of arr.


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


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


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

   Tillmann