5 ms·
Just to agree and emphasize, a more accurate title would probably be "Breaking eta equality breaks the monad laws." A lot of equational reasoning in general goe
by dwohnitmok 8y ago
Just to agree and emphasize, a more accurate title would probably be "Breaking eta equality breaks the monad laws." A lot of equational reasoning in general goes out the door at that point, not just monads.
More generally any kind of system that is able to introspect and differentiate between non-equivalent evaluations of itself tends to break a lot of invariants.
Imagine trying to establish equivalences between sequential and concurrent processes if the processes in question could introspect what thread it was running on and changed behavior based on that.
So yeah. Seq is what breaks things here. Not State. But even Haskell sometimes has to compromise purity for practicality.
- lmm 8y ago> even Haskell sometimes has to compromise purity for practicality. Well, the designers of Haskell made reasonable decisions based on what was known at the time. I'd argue that Idris shows that we don't have to make this particular compromise any more (and, more generally, that the result of Haskell's lazy-by-default experiment is negative).
- yvdriess 8y agoI would say 'by-demand lazy' failed. The by-demand implementation gives a guarantee that an expression is never evaluated if it is not used. Other non-strict forms exist where every expression will be touched, but no guarantees are given on the ordering. MIT's pH Haskell dialect is an example of this.
- Guvante 8y agoI could never figure out how to parse something between evaluating inside out (strict) and outside in (lazy, well ignoring the complexity around multiple evaluations). Every informal definition I thought of seemed too weak to be useful. This was due to the core problem that generally speaking the coder needs to know if a particular expression will be evaluated using local reasoning (e.g. if I get here will `A` or `B` be evaluated) and without by-demand or strict you can't make that guarantee. Taking a quick look at pH it looks like they haven't figured out the semantics quite yet so that isn't a true answer to the question either. Have there been any other non-strict languages with well known semantics? (Excluding things like Prolog)
- kreetx 8y agoPlease speak for yourself regarding lazyness.
- TylerE 8y agoI've always thought that (Oca)ML got it right here: Strict by default, but full lazyiness easily available.
- lmm 8y agoAgreed, and I think that's where post-Haskell languages are going (I've already mentioned Idris).
- Bromskloss 8y agoSorry, I'm not too knowledgeable about these things. What is the strict-versus-lazy dichotomy? I wouldn't have thought that they had to do with each other.
- TylerE 8y agoStrict being the opposite of lazy - expressions are executed immediately. Like for instance, given an expression... x = foo(13) In a strict language foo(13) will be evaluated immediately. In a lazy evaluation model, x be 'the result of foo(13)', but foo(13) won't actually be evaluated until some expression forces evaluation, by, for instance, printing the value. This is a gross simplication... lazy can do some really neat things like having functions that return infinite streams. The function would theoretically never terminate, but in practice would be called via something like... for event in infinite_stream() .. do stuff .. if event == TERMINAL_VALUE: break
- Bromskloss 8y agoIs it side effects that creates the need for strictness?
- TylerE 8y agoI wouldn't say so, just efficiency. The cost of booking for laziness isn't free. While it can potentially pay dividends when you're able to avoid evaluation altogether, it isn't free.