monads and categoricity (newbie)

[Sean McIlroy]

hello

i'm not talking about "category theory" necessarily, although it's
certainly possible an answer could come from that quarter; i'm talking
about the kind of categoricity a formal theory possesses iff all of
its models are isomorphic to each other; the monads of course are
haskell monads, and the question is roughly this:

not all monads are isomorphic to each other; for instance some monads
can be made instances of MonadPlus while others can not; can somebody
exhibit a collection of supersets of the monad laws such that two
monads are isomorphic iff they satisfy the same set of extended
laws ?

i'm pretty sure this is what i need in order to finally feel
comfortable with the mysterious monad concept; i realize it's not the
kind of thing that normally gets asked in this group
(searching turned up no similar-seeming questions), but i thought i'd
better try anyway;

thanks if you can help

peace
stm

[Dirk Thierbach]

Sean McIlroy <namenob...@gmail.com> wrote:
> i'm not talking about "category theory" necessarily, although it's
> certainly possible an answer could come from that quarter; i'm talking
> about the kind of categoricity a formal theory possesses iff all of
> its models are isomorphic to each other;

That never happens unless the formal theory is "trivial" and admits either
everything as a model, or just a single model.

> not all monads are isomorphic to each other; for instance some monads
> can be made instances of MonadPlus while others can not; can somebody
> exhibit a collection of supersets of the monad laws such that two
> monads are isomorphic iff they satisfy the same set of extended
> laws ?

Not possible for the above reason.

> i'm pretty sure this is what i need in order to finally feel
> comfortable with the mysterious monad concept; i realize it's not
> the kind of thing that normally gets asked in this group (searching
> turned up no similar-seeming questions), but i thought i'd better
> try anyway;

Try to think differently. I don't know what level of maths education
you have, but you probably know what a vector space is, right? Now,
there are lots of vector spaces that are not isomorphic, because they
can for example have different dimensions. But that doesn't stop you
from treating all vector spaces in the same way wrt. to the operations.
The operations are a sort of API for vector spaces: You can add them,
multiply them with a scalar, and so on. In fact, that's the whole point
of the API. There's nothing gained by requiring all vector spaces to
be isomorphic, then you wouldn't have any models to do something interesting
with.

It's the same for monads: Any monad has an API (a very simple one)
that basically says 'A monad is an overloaded semicolon operator, i.e.
if you have two actions X and Y, you can say "X; Y", and it doesn't
matter if you say "(X; Y); Z" or "X; (Y; Z)". Also, you can assign
the result of an action X to a (immutable) Variable, and the same kind of
laws apply.'

That's all there is to it. If you're programming in an imperative
language, you're using a particular monad all the time, you just don't
call it by that name. It's nothing mysterious at all. Just like a
vector space is nothing mysterious at all, as a human, you operate in
a 3D-environment all the time. Calling it a "vector space" just makes the
API explicit, so you can work with different vector spaces, too. (2D, 4D,
whatever).

- Dirk

[Paul Rubin]

Sean McIlroy <namenob...@gmail.com> writes:
> not all monads are isomorphic to each other; for instance some monads
> can be made instances of MonadPlus while others can not; can somebody
> exhibit a collection of supersets of the monad laws such that two
> monads are isomorphic iff they satisfy the same set of extended
> laws ?

If you're familiar with the idea of monoids from abtract algebra
(monoids are like groups but without the additive inverse requirement),
then it turns out that monads are just monoids in the category of
endofunctors on the category of Haskell types, and the monoid axioms
imply the monad laws. There is a good sigfpe post about the
monoid-monad connection:

http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html

[Aatu Koskensilta]

Dirk Thierbach <dthie...@usenet.arcornews.de> writes:

> Sean McIlroy <namenob...@gmail.com> wrote:
>> i'm not talking about "category theory" necessarily, although it's
>> certainly possible an answer could come from that quarter; i'm talking
>> about the kind of categoricity a formal theory possesses iff all of
>> its models are isomorphic to each other;
>
> That never happens unless the formal theory is "trivial" and admits either
> everything as a model, or just a single model.

I'm not sure what you have in mind here. We don't usually regard
e.g. second-order arithmetic "trivial" even though it has only one model
(up to isomorphism). Also, a theory admitting everything as a model
won't be categorical -- not every two things are isomorphic, after all!

Outside logic we usually meet sets of sentences and their models only
in context of the definition of some class of structures. We have, for
instance, the group axioms and the class of structures that satisfy
these axioms, i.e. groups. These sort of axioms are of course not
usually categorical.

--
Aatu Koskensilta (aatu.kos...@uta.fi)

"Wovon man nicht sprechen kann, darüber muss man schweigen."
- Ludwig Wittgenstein, Tractatus Logico-Philosophicus