Опять про Monadability

[lomeo]

Допустим у нас есть тип (X a), где X ::= T x y z ... Тут важно, что "a" последнее.
Тогда если "a" хотя бы в одном конструкторе данных стоит слева от стрелки, то этот тип нельзя сделать функтором (instance Functor) так, чтобы соблюдались законы над функторами, нес па?

Comments

[lomeo.livejournal.com]

У меня на самом деле обрывочные сведения о ТК, и я вижу функтор так:

Пусть F - функтор (например, список). Тогда "a", о которой я говорил - это объект категории, над которой определён этот функтор.

Теперь рассмотрим закон об identity функторов:

F(id_a) = F(a)

По какой то причине, если в F "a" учавствует в контрвариантой позиции (что это, кстати, значит - учавствует?), то этот закон не соблюдается. Почему? Это основной вопрос.

Насчёт контрвариантного функтора никогда не слышал. Это что то вроде cmap :: (b -> a) -> (f a -> f b) ?

Тогда для комонад должно соблюдаться (по аналогии join <-> dup; return <-> eval)

return . f = fmap f . return => eval . cmap f = f . eval
join . fmap join = join . join => cmap dup . dup = dup . dup => cmap dup = dup

Это так, измышления, надо побаловаться.

Ещё надо посмотреть есть ли и такой и такой для типов a->a :)

[ex-ex-zhuzh.livejournal.com]

не понял по поводу id. это функция, а a -- тип. как они могут быть равны?

id_{F a} = F id_a -- такой закон есть, но такой закон есть и для контравариантных функторов. почему вы думаете, что его нет?

приставка «ко» возникает, когда переворачиваются стрелки. функтор, говоря языком программирования хаскель, переводит типы в типы, а функции в функции. кофунктор (то есть контравариантный функтор, так короче) делает то же самое, но стрелки функций направлены в обратную сторону.

class Functor f where
  map :: (a->b) -> (f a -> f b)

class Cofunctor cof where
  comap :: (a -> b) -> (cof b > cof a)

если у нас есть индексируемый контейнер, то его можно сделать функтором по типу элементов или кофунктором по типу индексов. аналогично, тип (->) -- функтор по типу результата и кофунктор по типу аргумента.

[lomeo.livejournal.com]

Да, я описАлся, конечно же id(F(a))

Я не говорил, что такого закона нет для контравариантных функторов, я сказал, что нельзя построить "правильный" (ко-)функтор для типа (a->), чтобы этот закон соблюдался. И хотел разобраться почему.

Я забыл, что типы функции - это тоже типы, и, следовательно, являются объектами в рассматриваемой категории. Спасибо за напоминание и следующее из него объяснение :) Ещё не до конца понял (я про аналогию тип=объект и функтор (a->b) -> (f a-> f b)), но додумаю пока сам. Если что спрошу :)

Остальное вроде как понятно.