On Fri, Jun 18, 2010 at 5:57 PM, Ryan Ingram <ryani.s...@gmail.com> wrote:
> 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"?
Well, there's DeepArrow. I'm not sure if it's minimal or anything,
but IIRC that was its purpose.
> 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
>
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
