Извините, если это уже обсуждалось.

Вопрос больше теоретический. Монады в хаскель пришли из теории категорий. В теории категорий монады связаны с функторами. Но в хаскеле класс Monad не требует от instance реализовывать класс Functor. Получается, что хаскель использует монады не совсем как в теории категорий. Иными словами я могу написать неправильную монаду.

Здравствуйте, Petrovv, Вы писали:

P>Вопрос больше теоретический. Монады в хаскель пришли из теории категорий. В теории категорий монады связаны с функторами. Но в хаскеле класс Monad не требует от instance реализовывать класс Functor. Получается, что хаскель использует монады не совсем как в теории категорий. Иными словами я могу написать неправильную монаду.

Раньше был связан, но написать неправильную монаду всё равно можно было. Монадические законы не проверяются компилятором.

Здравствуйте, Petrovv, Вы писали:

P>Получается, что хаскель использует монады не совсем как в теории категорий. Иными словами я могу написать неправильную монаду.

Из http://www.haskell.org/sitewiki/images/8/85/TMR-Issue13.pdf

In fact, monads in category theory are defined in terms of return, fmap, and
join (often called , T, and µ in the mathematical literature). Haskell uses the
equivalent formulation in terms of (>>=) instead of join since it is more convenient
to use; however, sometimes it can be easier to think about Monad instances in
terms of join, since it is a more “atomic” operation. (For example, join for the
list monad is just concat.) An excellent exercise is to implement (>>=) in terms
of fmap and join, and to implement join in terms of (>>=).
..
..
liftM :: Monad m => (a -> b) -> m a -> m b. This should be familiar;
of course, it is just fmap. The fact that we have both fmap and liftM is an
unfortunate consequence of the fact that the Monad type class does not require
a Functor instance, even though mathematically speaking, every monad is a
functor. However, fmap and liftM are essentially interchangeable, since it is
a bug (in a social rather than technical sense) for any type to be an instance
of Monad without also being an instance of Functor.

Здравствуйте, Petrovv, Вы писали:

P> Иными словами я могу написать неправильную монаду.
Проверка выполнения законов монады аналогична проблеме останова. Поэтому компилятором и не проверяется.

Более того, есть монады, для которых законы не выполняются, но все ими пользуются. QuickCheck, Random

Здравствуйте, Mirrorer, Вы писали:

M>Более того, есть монады, для которых законы не выполняются, но все ими пользуются. QuickCheck, Random

Random — не монада. QuickCheck — не монада. Конечно же законы монад выполняться для них не будут

Если серьёзно, то Gen в QuickCheck, конечно же не настоящая монада. А вот с Random не понял. Если ты про отдельный пакет MonadRandom, то Rand — вполне себе нормальная монада, т.к. её семантическая модель — это монада State.

Здравствуйте, lomeo, Вы писали:

L>Если ты про отдельный пакет MonadRandom, то Rand — вполне себе нормальная монада, т.к. её семантическая модель — это монада State.

Да, мне тов. palm mute уже на это указал.
просто запала в голову цитата из статьи
Programming with Arrows
John Hughes

Nevertheless, programmers do sometimes use monads which do not satisfy
the stated laws. Wadler’s original paper [26] introduced the “strictness monad”
whose only effect is to force sequencing to be strict, but (as Wadler himself
points out), the laws are not satisfied. Another example is the random generation
“monad” used in our QuickCheck [4] testing tool, with which terms equivalent
by the monad laws may generate different random values — but with the same
distribution. There is a sense in which both these examples “morally” satisfy the
laws, so that programmers are not unpleasantly surprised by using them, but
strictly speaking the laws do not hold

Здравствуйте, Mirrorer, Вы писали:

M>Проверка выполнения законов монады аналогична проблеме останова. Поэтому компилятором и не проверяется.

Для _произвольной_ программы и монады это наверное так. Но например в dependent type языке и программы гарантированно завершаются и монадные законы выполняются. Вот в Agde например так:

Compare this type of definition with Haskell where we can define the operations of a monoid and define an
instance of a monoid (e.g. natural numbers, zero and addition) but we cannot show inside the system that
this instance would obey the laws of a monoid. In Agda we can do both: we can write programs that make
use of algebraic structure and we can reason about them, and in the process make extra guarantees that
the we really have the structures that we say we do.

Интересно, а монаду в хаскеле в dependent-type стиле можно записать? А то SafeList-ы при помощи чисел Пеано — это конечно прикольно, но как насчет чего-нить покруче?