Будет ли иметь смысл класс типов между категорией и стрелкой?

Часто у вас есть что-то вроде Applicative без pure или что-то вроде Monad, но без return. Пакет semigroupoid охватывает эти случаи с 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)) необратим. Тем не менее, как вы думаете, может ли этот более слабый класс типов быть полезным? Имеет ли это смысл даже с теоретической точки зрения?


typeclass haskell arrows category-abstractions
person Landei    schedule 09.08.2011    source источник
comment
Разве Arrow функции не являются точно определением категории?   -  person Alexandre C.    schedule 09.08.2011
comment
Нет, функции Category — это определение категории. Ну, в любом случае морфизмы (и никаких законов) — насколько я понимаю, Category соответствует подкатегории Hask, которая имеет те же объекты (всех типов), но разные морфизмы. Arrow добавляет гораздо больше структуры, но я не знаю достаточно, чтобы что-то сказать о том, что это за структура.   -  person Antal Spector-Zabusky    schedule 09.08.2011
comment
@Antal S-Z: На самом деле это не подкатегория. Category указывает категорию, объекты которой являются объектами Hask со стрелками, заданными некоторым конструктором двумерного типа. Functor описывает подкатегорию Hask, стрелки которой являются стрелками Hask с объектами, заданными некоторым конструктором одномерного типа. Applicative сопоставляет моноидальную структуру (,) с Functor, а (&&&) и т. д. сопоставляет ее с Category. И arr дает функтор от Hask до Category.   -  person C. A. McCann    schedule 09.08.2011
comment
@Antal S-Z: Кроме того, ArrowApply делает декартово Category закрытым, предоставляя всю мощь лямбда-исчисления со стрелками более высокого порядка, каррированием и т. д., а также возможность отображать все это из Hask в Category. Стрелки от неподвижного объекта дают тогда обычную монадную структуру Reader, вот почему Kleisli m a b изоморфна ReaderT a m b.   -  person C. A. McCann    schedule 09.08.2011
comment
@C.A.: Спасибо, понятно. Я изучаю CS, но пока только дилетант в CT (если что). Надеюсь, это изменится.   -  person Antal Spector-Zabusky    schedule 09.08.2011
comment
@Antal S-Z: я сам не более чем дилетант, которого достаточно, чтобы переводить основные понятия между математическими описаниями и реализациями Haskell. Увы, меня все еще сильно смущают высокоуровневые обобщения и свойства категорий, не похожие на Haskell, поскольку вся моя интуиция идет со стороны программирования.   -  person C. A. McCann    schedule 09.08.2011
comment
@C.A.McCann Я знаю, что это старый вопрос, но я только что нашел его во время поиска в Google. ArrowApply не делает категорию декартовой замкнутой, поскольку аксиомы Arrows не создают произведения кортежей.   -  person Anonymous    schedule 20.12.2011
comment
@Anonymous: Вы совершенно правы. Если мне не изменяет память, довольно много конкретных экземпляров Arrow действительно не имеют продуктов.   -  person C. A. McCann    schedule 20.12.2011

Ответы (2)


arrow_upward
10
arrow_downward

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

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

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

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

person sclv    schedule 09.08.2011

arrow_upward
9
arrow_downward

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

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

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

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

person C. A. McCann    schedule 09.08.2011
comment
Не существует принципиального способа написать &&& вместо Rev (или Iso, если хотите). Почему ты спрашиваешь? Потому что b -> a и c -> a не дают вам никакого способа получить (b,c) -> a так, что ваши a -> b и a -> c оба гарантированно вернут ваши исходные b и c. - person sclv; 09.08.2011
comment
Точно так же вы не можете написать правильные fst и snd для Iso! Что является обратным к (a,b) -> a? Вот почему вам нужны частичные изоморфизмы. (Конечно, вы можете написать first и second, однако). - person sclv; 09.08.2011
comment
@sclv: Ага. Фактически, и (***), и (+++) должны подойти, как и функции, дающие ассоциативные, коммутативные и дистрибутивные свойства типов произведения/суммы. Но (&&&) и (|||) в общем случае работать не могут. - person C. A. McCann; 09.08.2011
comment
Упс, сначала неправильно прочитал ваш пост. Мы в жестоком согласии :-) - person sclv; 09.08.2011
comment
Без проблем. Это полезное разъяснение того, почему что-либо, напоминающее категориальный продукт, не может работать. Стрелки должны сохранять информацию, вероятно, давая что-то вроде линейной логики вместо привычной нам интуиционистской логики. - person C. A. McCann; 09.08.2011