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 <ekm...@gmail.com> wrote:
> 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
>
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
