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