MonadSum

[voidex]

Подумалось мне про трансформеры монад, что если у нас есть натуральные преобразования из монад m и n в некую монаду l, то l - это их сумма, если добавить ещё и обратную функцию. Т.е. при наличии натурального преобразования m => t и n => t можем получить и m+n => t.

Попробовал я это представить прямо в таком виде:

data MonadSum m n a = MonadSum

Comments

[beroal]

Ваши функции типов forall b. m b -> t b, forall c. n c -> t c - это морфизмы монад или что?

[voidex]

Да, морфизм монад:

lift : m => t -- натуральное преобразование

при этом, как я понимаю, должны выполняться:

return = lift . return
join . lift . map lift = lift . join

Ко мне можно на ты

[beroal]

Пока что я не вижу, какое отношение MonadSum m n имеет к сумме в категории монад и морфизмов монад. И не уверен, что сумма всегда существует.

[voidex]

У нас есть морфизмы n => MonadSum n m и m => MonadSum n m, и при наличии n => t и m => t можем построить MonadSum n m => t

Точно так же можно представить Either:

data Either a b = Either {
either :: forall c. (a -> c) -> (b -> c) -> c }

Или я несу чушь?

[beroal]

Чтобы доказать, что, например, liftL является морфизмом монад, надо иметь доказательство, что содержимое MonadSum m n a принимает только морфизмы монад, и взять его неоткуда. А без доказательств это просто кусок кода, который непонятно зачем нужен.

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

[voidex]

Ну в Haskell и instance Monad тоже не монада.
Что такое ССС?

[beroal]

Ну в Haskell и instance Monad тоже не монада.
Чего? Haskell, конечно, не требует доказательств, но люди обычно доказывают. А тех, кто не доказывает, осаживают.

Что такое ССС?
Cartesian closed category

[voidex]

> Чего? Haskell, конечно, не требует доказательств, но люди обычно доказывают. А тех, кто не доказывает, осаживают.
Ну т.е. это на совести людей, тут также. Хотя в Агде я могу потребовать именно морфизмов монад со всеми доказательствами.

[beroal]

Так как понимать «в Haskell instance Monad не монада»?

[voidex]

Monad m не гарантирует, что m - монада, в той же степени, что и (Monad m, Monad n) не гарантирует, что (forall a. m a -> n a) - морфизм монад.