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