a question on mathovervlow

[Vlad Patryshev]

http://mathoverflow.net/questions/85391/any-example-of-a-non-strong-monad
I was absolutely impressed with the answers

Thanks,
-Vlad

[Valeria de Paiva]

Nice!

> --
> You received this message because you are subscribed to the Google Groups
> "Bay Area Categories And Types" group.
> To post to this group, send email to ba...@googlegroups.com.
> To unsubscribe from this group, send email to
> bacat+un...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/bacat?hl=en.

--
Valeria de Paiva
http://www.cs.bham.ac.uk/~vdp/
http://valeriadepaiva.org/www/

[Arthur Chan]

So correct me if I'm wrong but the way I interpreted the answers is, there aren't any non-strong in the programming models we are used to, or at least the way to fmap does not involve a simple function. Most of the well known examples of functors (e.g. Maybe and State) live within Haskell's usual semantics, oblivious of the "outside world," for lack of better language. And that interesting examples of this will show up in distributed computing models, where we do not have "Gamma".

Arthur :: LittleBrick

[Vlad Patryshev]

See, if the category is well-pointed, every monad is strong.
Now, I've also found a pretty simple example of a monad that is not strong - of course in a non-well-pointed topos. And this is a pretty serious case: this topos, Set^2, represents a three-valued logic (can talk about it later at a meeting) that is pretty practical.

We probably should go further and try to build a system where we could demonstrate this more clearly.

Valeria, I believe this kind of logic is your area, right? Would be cool to build a Haskell that does not have LiftM2. :) Also, I'm still curious, a well-pointed topos, should it be boolean, or not necessarily?

Thanks,
-Vlad

[Valeria de Paiva]

Vlad,
the way I see it, it's not a big deal. People who care for toposes
know that they're are not necessarily well-pointed and that they're
not necessarily Boolean and some take this as evidence that
constructive logic is a better basis to build our mathematical
theories on.

People who believe that Boolean logic is the only one worth
considering, will probably not pay attention to examples of
non-well-pointed toposes or non-strong monads or even Haskell models
of any thing. and they probably don't care for 3-valued logics of any
kind.

it's nice to know that one needs to look outside Sets to find a
non-strong monad(it was a good question). and it's nice to know that
the monads arising from continuations and resumptions are not
necessarily strong, but I don't conclude anything else from these two
facts.

Also the fact that a Diamond S4 is the logical contents of a free
monad is the essence of my paper with Nick Benton and Gavin Bierman in
JFP 1998:
N Benton, G Bierman and V de Paiva. Computational Types from a Logical
Perspective. Journal of Functional Programming 8(2):177-193 March
1998. © Cambridge University Press 1998.
available from Nick's page
http://research.microsoft.com/en-us/um/people/nick/publications.htm
long before "A Symmetric Modal Lambda Calculus for Distributed
Computing" in lics 2004.

now I haven't read the latter, so maybe I should, but the way I see
it, the modeling of distributed computing is not set in stone, it's
simply a proposal with pros and cons, while the Curry-Howard
correspondence in the former is a mathematical theorem. but maybe I
should shut up and read.

cheers,
Valeria

[Vlad Patryshev]

Valeria,

I'll read it, thanks a lot! And besides, good point, once we have distributed calculations, we lose booleanness, we probably lose well-pointedness, functorial strengh, and, hense, LiftM2 that is so essential in Haskell. Good point!

Thanks,
-Vlad