On Wed, Jun 16, 2010 at 6:55 AM, Tillmann Rendel <
ren...@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
