On 23 Dec 2011, at 16:16, MigMit wrote:
On 23 Dec 2011, at 02:11, Conor McBride wrote:
So... you are developing a programming language with all calculations being automatically lifted to a monad? What if we want to do calculations with monadic values themselves, like, for example, store a few monadic calculations in a list (without joining all there effects as the sequence function does)?
The plan is to make a clearer distinction between "being" and "doing" by splitting types clearly into an effect part and a value part, in a sort of a Levy-style call-by-push-value way. The notation
[<list of effects>]<value type>
is a computation type whose inhabitants might *do* some of the effects in order to produce a value which *is* of the given value type.
Oh, so it's not an arbitrary monad, but a single one. That's a bit disappointing.
The list of effects is arbitrary, and localizable, by means of defining handlers. So it's not a single monad. It's probably still disappointing. Cheers Conor