Опять про Monadability

[lomeo]

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

Comments

[deni-ok.livejournal.com]

Расшифруй про тип. Глупый, не понимаю, где a последнее?

[lomeo.livejournal.com]

Ну например тип

data T x y z a = ... | C (a -> x)

instance Functor (T x y z)

В (data T x y z a) как ты видишь "а" последнее

[thesz.livejournal.com]

Yep. ;)

[ex-ex-zhuzh.livejournal.com]

а почему такой вопрос возник?

[lomeo.livejournal.com]

Пробовал сделать монадой такой тип, показалось, что это упростит обработку, не получилось, стал разбираться - пришёл к такому выводу.

В принципе, мне этот тип как монада и не нужен, просто стало интересно почему так.

[ex-ex-zhuzh.livejournal.com]

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

[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)), но додумаю пока сам. Если что спрошу :)

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

[migmit.livejournal.com]

Ну, если

data X a = X ((a -> Int) -> Int)
, то можно, и очень легко. Более того, это монада.

[lomeo.livejournal.com]

Блин, точно, спасибо тебе.

А как вообще тогда определить? Ты можешь мне объяснить как на ТК ложатся типы? В смысле не просто тип X, а его расшифровка - (a -> Int) -> Int - это что в ТК?

Re: Reply to your comment...

[migmit.livejournal.com]

Есть такое понятие "декартово замкнутая категория". Точное определение - это категория, в которой 1) есть бинарные произведения - аналог типов (X,Y), и 2) функтор (-,X) имеет правый сопряжённый, который мы можем обозначить через (X ->). Про сопряжённые функторы знаешь?
Дык вот, в декартово замкнутой категории написать такой функтор (в смысле, (a -> X) -> X, где X - какой-то фиксированный объект) - нет проблем. Более того, это опять будет монада.

Re: Reply to your comment...

[lomeo.livejournal.com]

Про сопряженные функторы знаю, а что такое (-,X)? В смысле "-" что означает?

Может где то можно почитать про отображение типов Хаскеля на ТК?

Re[2]: Reply to your comment...

[migmit.livejournal.com]

Параметр. То есть, это функтор, переводящий объект Y в объект (Y,X).
Почитать - не знаю, я в своё время задавал аналогичный вопрос в ru_lambda, относительно "введения в Хаскель для знающих теорию категорий", не нашли.

Re: Re[2]: Reply to your comment...

[lomeo.livejournal.com]

Ясно, спасибо большое. Тогда буду тебя допекать ;)

А как ты разбирался? Вот, например, как ты догадался / где узнал то, что объяснил мне?

Re[4]: Reply to your comment...

[migmit.livejournal.com]

Допекай, я не против.
Я уже знал ТК на неплохом уровне, когда обнаружил Хаскель. А когда что-то хорошо знаешь, начинаешь видеть аналогии и прямые совпадения. Ну и, плюс, терминология помогает - не зря же монаду монадой назвали, как раз из ТК название и пришло.

Re: Re[4]: Reply to your comment...

[lomeo.livejournal.com]

OK :-) Тогда буду усиленнее вгрызаться в ТК :)