haskell - Flecha sin arr

arrows category-theory

Question

Si restringimos nuestra comprensión de una categoría para que sea la Category habitual en Haskell:

class Category c where
  id :: c x x
  (>>>) :: c x y -> c y z -> c x z

Entonces digamos que una Arrow es una Category que además puede:

class Category c => Arrow c where
  (***) :: c x y -> c x'' y'' -> c (x,x'') (y,y'')
  (&&&) :: c x y -> c x y'' -> c x (y,y'')

Podemos derivar fácilmente:

first :: c x y -> c (x,z) (y,z)
first a = a *** id

second :: c x y -> c (z,x) (z,y)
second a = id *** a

O podemos derivar (***) de first y second :

a1 *** a2 = first a1 >>> second a2

También podemos derivar:

dup :: c x (x,x)
dup = id &&& id

O podemos derivar (&&&) dado dup y (***) :

a1 &&& a2 = dup >>> (a1 *** a2)

¿Cuál es mi punto y cuál es mi pregunta? Es esto:

¿Qué es la Arrow sin arr ? Parece perfectamente coherente y útil. ¿Existen leyes de flecha (aparte de las leyes de categoría) que no implican arr y permanecen intactas aquí? ¿Y qué significa todo esto en la teoría de categorías?

Básicamente robé esta pregunta de reddit, pero la generalicé y expuse en ella: http://www.reddit.com/r/haskell/comments/2e0ane/category_with_fanout_and_split_but_not_an_arrow/

Answer 1

Del mismo modo que Arrow es una categoría con producto, Arrow sin arr también es una categoría con producto (por lo tanto, las leyes de categoría siempre se cumplen).

arr es un functor de la categoría Hask a la categoría c . El código que se muestra a continuación indica esto. arr proporciona una forma de elevar las funciones normales (que son morfismos en Hask) a la categoría c instanciada. Esto es algo así como fmap ( fmap de Hask a Hask) pero más generalizado. En relación con esto, algunas de las leyes de flecha here describen las leyes de functor (aunque también existen las leyes para el producto).

Entonces, al omitir arr , se pierde la función de levantar funciones normales o, desde otro punto de vista, se libera de su implementación. Sin embargo, todas las demás características son las mismas.

{-# LANGUAGE TypeOperators, RankNTypes #-}

-- | Functor arrow
type (:->) c d = forall a b. c a b -> d a b

-- | Hask category; types are objects, functions are morphisms.
type Hask = (->)

arr :: Arrow c => Hask :-> c
arr = Control.Arrow.arr