Есть ли вещь, называемая "полу-монадой" или "контр-монадой"?

Хорошо, я изучаю Монастыри Хаскелла. Когда я прочитал статью Wikibook , я обнаружил, что подпись морфологий монад выглядит довольно похожей на тавтологию в логике, но вам нужно преобразовать M a в ~~A, здесь ~ - это логическое отрицание.

return :: a -> M a -- Map to tautology A => ~~A, double negation introduction
(>>=) :: M a -> (a -> M b) -> M b -- Map to tautology ~~A => (A => ~~B) => ~~B

другие операции также являются тавтологиями:

fmap :: (a -> b) -> M a -> M b -- Map to (A => B) -> (~~A => ~~B)
join :: M (M a) -> M a -- Map to ~~(~~A) => ~~A

Также понималось, что в соответствии с тем, что соответствие нормальных функциональных языков Curry-Howard - это интуитивная логика, а не классическая логика, поэтому мы не можем ожидать тавтологии например, ~~A => A может иметь соответствие.

Но я думаю о чем-то другом. Почему Монада может относиться только к двойному отрицанию? что соответствует единственному отрицанию? Это привело меня к следующему определению класса:

class Nomad n where
    rfmap :: (a -> b) -> n b -> n a
    dneg :: a -> n (n a)

return :: Nomad n => a -> n (n a)
return = dneg
(>>=) :: Nomad n => n (n a) -> (a -> n (n b)) -> n (n b)
x >>= f = rfmap dneg $ rfmap (rfmap f) x

Здесь я определил понятие "Nomad" и поддерживает две операции (оба связаны с логической аксиомой в интуитивной логике). Обратите внимание, что имя "rfmap" означает тот факт, что его подпись похожа на функтор fmap, но порядок a и b отменяется в результате. Теперь я могу переопределить операции Monad с ними, заменив M a на n (n a).

Итак, теперь отпустите часть вопроса. Тот факт, что Монада является концепцией теории категорий, по-видимому, означает, что мой "Кочевник" также является концепцией теории категорий. Так что это? Это полезно? Существуют ли какие-либо документы или результаты исследований в этой теме?

Ответы

Ответ 1

Двойное отрицание - это особая монада

data Void --no constructor because it is uninhabited

newtype DN a = DN {runDN :: (a -> Void) -> Void}

instance Monad DN where
   return x = DN $ \f -> f x
   m >>= k  = DN $ \c -> runDN m (\a -> runDN (k a) c))

на самом деле, это пример более общей монады

type DN = Cont Void
newtype Cont r a = Cont {runCont :: (a -> r) -> r}

который является монадой для продолжения прохождения.

Концепция типа "монада" не определяется только сигнатурой, но также некоторыми законами. Итак, вот вопрос, какими должны быть законы для вашего строительства?

(a -> b) -> f b -> f a

является сигнатурой метода, хорошо известного теории категорий, контравариантного функтора. Он подчиняется по существу тем же законам, что и функторы (сохраняет (со) состав и идентичность). На самом деле контравариантный функтор точно является функтором противоположной категории. Поскольку нас интересуют "функторы haskell", которые, как предполагается, являются эндо-функторами, мы видим, что "контрацептивный функтор" haskell "является функтором Hask -> Hask_Op.

С другой стороны, как насчет

a -> f (f a)

какие законы должны иметь это? У меня есть предложение. В теории категорий можно сопоставить между Функторами. Учитывая два функтора из F, G каждого из категории C в категорию D, естественное преобразование от F до G является морфизмом в D

forall a. F a -> G a

который подчиняется некоторым законам когерентности. Вы можете многое сделать с естественными преобразованиями, включая их использование для определения категории "функтора". Но классическая шутка (из-за Mac Lane) заключается в том, что категории были изобретены, чтобы говорить о функторах, были изобретены функторы, чтобы говорить о естественных преобразованиях, и естественные преобразования были изобретены, чтобы говорить о дополнениях.

Функтор F : D -> C и функтор G : C -> D образуют присоединение от C до D, если существуют два естественных преобразования

unit : Id -> G . F
counit : F . G -> Id

Эта идея присоединения является частым способом понимания монадов. Каждое присоединение порождает монаду совершенно естественным образом. То есть, поскольку состав этих двух функторов является эндофунктором, и у вас есть что-то похожее на возврат (единица), все, что вам нужно, это соединение. Но это легко, объединение - это просто функция G . F . G . F -> G . F, которую вы получаете, просто используя конкатент "посередине".

Итак, тогда со всем этим, что вы ищете? Хорошо

dneg :: a -> n (n a)

выглядит точно так же, как unit присоединения контравариантного функтора с самим собой. Таким образом, ваш тип Nomad вероятен (конечно, если ваше использование его для построения монады является правильным) точно так же, как "контравариантный функтор, который является самосопряженным". Поиск самосопряженных функторов приведет вас к двойному отрицанию и продолжению передачи..., который именно там мы и начали!

EDIT: почти наверняка некоторые из вышеперечисленных стрелок назад. Однако основная идея правильная. Вы можете использовать это самостоятельно, используя приведенные ниже цитаты:

Лучшие книги по теории категорий, вероятно,

  • Стив Awodey, Теория категорий
  • Sanders Mac Lane, Категории для рабочего математика

хотя существует множество более доступных интро-книг, в том числе книга Бенджамина Пирса по теории категорий для компьютерных ученых.

Видео-лекции онлайн

В ряде работ исследуется угол присоединения на продолжении монады, например

  • Хайо Тилеке, продолжение Семантика и самосопряженность

Поисковые термины "самосопряженные", "продолжение" и "монада" хороши. Кроме того, ряд блоггеров написал об этих проблемах. Если вы google "откуда происходят монады", вы получаете полезные результаты, например этот из кафе n категории, или этот из sigfpe. Также ссылка Sjoerd Vissche читателю Comonad.

Ответ 2

Это был бы самосопряженный контравариантный функтор. rfmap предоставляет контравариантную часть функтора, а dneg - единичный и кассиент присоединения.

Op r - пример, который создает монаду продолжения. См. Контравариантные модули в http://hackage.haskell.org/package/adjunctions для некоторого кода.

Вы должны прочитать http://comonad.com/reader/2011/monads-from-comonads/, что связано и очень интересно.