Имеет ли смысл тип класса "между" Category и Arrow? - PullRequest
Новая
       27

Имеет ли смысл тип класса "между" Category и Arrow?

16 голосов
/ 09 августа 2011

Часто у вас есть что-то вроде Applicative без pure или что-то вроде Monad, но без return. Пакет полугрупоид охватывает эти случаи с Apply и Bind. Сейчас я нахожусь в аналогичной ситуации, касающейся Arrow, где я не могу определить значимую arr функцию, но я думаю, что другие функции имели бы смысл.

Я определил тип, который содержит функцию, и это обратная функция: 

import Control.Category

data Rev a b = Rev (a -> b) (b -> a)

reverse (Rev f g) = Rev g f
apply (Rev f _) x = f x
applyReverse (Rev _ g) y = g y
compose (Rev f f') (Rev g g') = Rev ((Prelude..) f g) ((Prelude..) g' f') 

instance Category Rev where
  id = Rev Prelude.id Prelude.id
  (.) x y = compose x y

Теперь я не могу реализовать Arrow, но что-то более слабое: 

--"Ow" is an "Arrow" without "arr"
class Category a => Ow a where
  first :: a b c -> a (b,d) (c,d)
  first f = stars f Control.Category.id

  second :: a b c -> a (d,b) (d,c)
  second f = stars Control.Category.id f

  --same as (***)
  stars :: a b c -> a b' c' -> a (b,b') (c,c')

 ...
 import Control.Arrow 

 instance Ow Rev where
    stars (Rev f f') (Rev g g') = Rev (f *** g) (f' *** g')

Я думаю, что не могу реализовать эквивалент &&&, так как он определен как f &&& g = arr (\b -> (b,b)) >>> f *** g, а (\b -> (b,b)) необратим. Тем не менее, вы думаете, этот класс более слабого типа может быть полезным? Имеет ли это смысл с теоретической точки зрения?

Ответы [ 2 ]

10 голосов
/ 09 августа 2011

Этот подход был рассмотрен в статье «Туда и обратно: стрелки для обратимого программирования»: http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.153.9383

Именно по тем причинам, с которыми вы сталкиваетесь, это оказалось плохим подходом, который не былподнят более широко.Совсем недавно Тильманн Рендель разработал восхитительный подход к обратимому синтаксису, который заменил частичные изоморфизмы на биарроу (http://www.informatik.uni -marburg.de / ~ rendel / rendel10invertible.pdf ).Это было упаковано для взлома, чтобы люди могли использовать и играть с ним: http://hackage.haskell.org/package/invertible-syntax

Тем не менее, я думаю, что стрелка без arr имеет определенный смысл.Я просто не думаю, что такая вещь является подходящим средством для захвата обратимых функций.

Редактировать : Есть также Обобщенные стрелки Адама Мегача (http://www.cs.berkeley.edu/~megacz/garrows/). Они, возможно, бесполезны для обратимыхпрограммирование тоже (хотя базовый класс типов действительно кажется обратимым), но они действительно используются в других ситуациях, когда arr слишком сильный, но другие операции со стрелками могут иметь смысл.

9 голосов
/ 09 августа 2011

С точки зрения теории категорий, класс типов Category описывает любую категорию, стрелки которой могут быть просто описаны в Haskell конструктором типов.Практически любая дополнительная функция, которую вы хотите построить поверх нее, в виде новых примитивных стрелок или функций построения стрелок, будет в некоторой степени иметь смысл, если вы сможете реализовать ее, используя общие функции.Единственное предостережение в том, что добавление выразительной силы может нарушить другие требования, как это часто бывает с arr.

. Ваш конкретный пример обратимых функций описывает категорию, в которой все стрелки являются изоморфизмами.В шокирующем повороте полностью и полностью ожидаемого, у Эдварда Кметта уже есть реализация этой в Hackage.

Функция arr примерно равна функтору (в смысле теории категорий) из функций Haskell в экземпляр Arrow, оставляя объекты одинаковыми (то есть параметры типа).Простое удаление arr из Arrow дает вам ... что-то еще, что, вероятно, само по себе не очень полезно, по крайней мере без добавления эквивалентов arr fst и arr snd в качестве примитивов.

Я считаю, что добавление примитивов для fst и snd вместе с (&&&) для построения новой стрелки из двух входов должно дать вам категорию с products , что абсолютно разумно с теоретической точки зрениязрения, а также несовместимости с обратимыми стрелками, которые вы используете, по причинам, которые вы нашли.

...