On Sat, Jan 21, 2012 at 10:08 AM, Roman Cheplyaka wrote:

* David Barbour [2012-01-21 10:01:00-0800]

...

As noted, IO is not strict in the value x, only in the operation that generates x. However, should you desire strictness in a generic way, it would be trivial to model a transformer monad to provide it.

Again, that wouldn't be a monad transformer, strictly speaking, because "monads" it produces violate the left identity law.

It meets the left identity law in the same sense as the Eval monad from Control.Strategies. http://hackage.haskell.org/packages/archive/parallel/3.1.0.1/doc/html/src/Co... That is, so long as values at each step can be evaluated to WHNF, it remains true that `return x >>= f` = f x. I did mess up the def of >>=. I think it should be: (StrictT op) >>= f = StrictT (op >>= \ x -> x `seq` runStrictT (f x)) But I'm not interested enough to actually pull out an interpreter and test... Regards, Dave

On Sat, Jan 21, 2012 at 10:51 AM, David Menendez wrote:

The Eval monad has the property: return undefined >>= const e = e.

You can't write `const e` in the Eval monad.

From what I can tell, your proposed monads do not.

You can't write `const e` as my proposed monad, either. Regards, Dave

On Sat, Jan 21, 2012 at 11:08 AM, Roman Cheplyaka wrote:

* David Barbour [2012-01-21 11:02:40-0800]

...

On Sat, Jan 21, 2012 at 10:51 AM, David Menendez wrote:

...

The Eval monad has the property: return undefined >>= const e = e.

You can't write `const e` in the Eval monad.

Why not?

ghci> runEval $ return undefined >>= const (return ()) ()

It is, at the very least, utterly pointless to have an Eval monad with `const`. Regards, Dave

* David Barbour [2012-01-21 11:09:43-0800]

Logically only has meaning when `=` applies to values in the domain. `undefined` is not a value in the domain.

We can define monads - which meet monad laws - even in strict languages.

In strict languages 'undefined' is not a value in the domain indeed, but it is in non-strict languages, exactly because they are non-strict. I think that's what Robert Harper meant by saying that Haskell doesn't have a type of lists, while ML has one [1]. [1]: http://existentialtype.wordpress.com/2011/04/24/the-real-point-of-laziness/ -- Roman I. Cheplyaka :: http://ro-che.info/

observably different from `undefined`

If we understand `undefined` as meaning a computation that never ends, then you cannot ever observe whether one `undefined` is or is not equivalent to another. In strict languages, this is especially obvious. In any case, I don't accept a concept of `monads` that changes so drastically based upon the host language. The laws for monads only apply to actual values and combinators of the monad algebra - and, since `undefined` is not a value, it need not apply. Similarly, algebraic laws for integer arithmetic don't need to account for `undefined`. And our geometry abstractions and theorems don't need to account for `undefined`. Attempting to shoehorn `undefined` into your reasoning about domain algebras and models and monads is simply a mistake. Regards, Dave On Sun, Jan 22, 2012 at 6:49 AM, Sebastian Fischer wrote:

On Sat, Jan 21, 2012 at 8:09 PM, David Barbour wrote:

...

In any case, I think the monad identity concept messed up. The property: return x >>= f = f x

Logically only has meaning when `=` applies to values in the domain. `undefined` is not a value in the domain.

We can define monads - which meet monad laws - even in strict languages.

In strict languages both `return undefined >>= f` and `f undefined` are observably equivalent to `undefined` so the law holds.

In a lazy language both sides might be observably different from `undefined` but need to be consistently so. The point of equational laws is that one can replace one side with the other without observing a difference. Your implementation of `StrictT` violates this principle.

Sebastian

2012/1/22 MigMit

Отправлено с iPad

22.01.2012, в 20:25, David Barbour написал(а):

...

Attempting to shoehorn `undefined` into your reasoning about domain algebras and models and monads is simply a mistake.

No. Using the complete semantics — which includes bottoms aka undefined — is a pretty useful technique, especially in a non-strict language.

It is a mistake. You mix semantic layers - confusing the host language with the embedded language. If you need to model non-termination or exceptions or the like, you should model them explicitly as values in your model. That is, *each* layer of abstraction that needs `undefined` should explicitly have its own representation for such concepts, rather than borrowing implicitly from the host. Regards, Dave

Thanks for the reference. I base my opinion on my own observations - e.g. the repeated failures of attempting to model stream processing with infinite lists, the relative success of modeling exceptions explicitly with monads compared to use of `fail` or SomeException, etc.. On Mon, Jan 23, 2012 at 6:29 AM, Sebastian Fischer wrote:

On Sun, Jan 22, 2012 at 5:25 PM, David Barbour wrote:

...

The laws for monads only apply to actual values and combinators of the monad algebra

You seem to argue that, even in a lazy language like Haskell, equational laws should be considered only for values, as if they where stated for a total language. This kind of reasoning is called "fast and loose" in the literature and the conditions under which it is justified are established by Danielsson and others:

http://www.cse.chalmers.se/~nad/publications/danielsson-et-al-popl2006.html

Sebastian

Space leaks, time leaks, resource leaks, subtle divergence issues when filtering lists, etc. On Mon, Jan 23, 2012 at 11:57 AM, Jake McArthur wrote:

On Mon, Jan 23, 2012 at 10:45 AM, David Barbour wrote:

...

the repeated failures of attempting to model stream processing with infinite lists,

I'm curious about what failures you're talking about.

- Jake

Evaluating the argument/result was my intention. Evaluating the computation itself might be useful in some cases, though. Regards, Dave On Sat, Jan 21, 2012 at 3:20 PM, Yves Parès wrote:

...

(StrictT op) >>= f = StrictT (op >>= \ x -> x `seq` runStrictT (f x))

Are you sure? Here you evaluate the result, and not the computation itself. Wouldn't it be:

(StrictT op) >>= f = op ` seq` StrictT (op >>= \x -> runStrictT (f x))

??

2012/1/21 David Barbour

...

On Sat, Jan 21, 2012 at 10:08 AM, Roman Cheplyaka wrote:

...

* David Barbour [2012-01-21 10:01:00-0800]

...

As noted, IO is not strict in the value x, only in the operation that generates x. However, should you desire strictness in a generic way, it would be trivial to model a transformer monad to provide it.

Again, that wouldn't be a monad transformer, strictly speaking, because "monads" it produces violate the left identity law.

It meets the left identity law in the same sense as the Eval monad from Control.Strategies.

http://hackage.haskell.org/packages/archive/parallel/3.1.0.1/doc/html/src/Co...

That is, so long as values at each step can be evaluated to WHNF, it remains true that `return x >>= f` = f x.

I did mess up the def of >>=. I think it should be: (StrictT op) >>= f = StrictT (op >>= \ x -> x `seq` runStrictT (f x))

But I'm not interested enough to actually pull out an interpreter and test...

Regards,

Dave

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On 21/01/2012 18:08, Steve Horne wrote:

Even so, to see that strictness isn't the issue, imagine that (>>=) were rewritten using a unary executeActionAndExtractResult function. You could easily rewrite your lamba to contain this expression in place of x, without actually evaluating that executeActionAndExtractResult. You'd still be doing a form of composition of IO actions. And when you finally did force the evaluation of the complete composed expression, the ordering of side effects would still be preserved - provided you only used that function as an intermediate step in implementing (>>=) at least.

Doh!!! - that function *does* exist and is spelled "unsafePerformIO". But AFAIK it isn't used for compilation/interpretation of (>>=) operators. If it *were* used, the rewriting would also need an extra "return". So... a >>= b -> f b becomes... return (f (unsafePerformIO a))