Опять про Monadability

[lomeo]

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

Comments

[deni_ok]

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

[lomeo]

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

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

instance Functor (T x y z)

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

[thesz]

Yep. ;)

[ex_ex_zhuzh]

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

[lomeo]

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

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

[ex_ex_zhuzh]

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

[lomeo]

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

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

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

F(ida) = 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 :)

[migmit]

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

[lomeo]

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

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

Re: Reply to your comment...

[migmit]

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

Re: Reply to your comment...

[lomeo]

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

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