
Excerpts from Heinrich Apfelmus's message of Mon Apr 25 04:01:03 -0400 2011:
The thing is that lazy evaluation is referentially transparent while "I don't care about [(1,4),(2,2)] vs [(2,2),(1,4)]" is not.
Perhaps more precisely, laziness's memoization properties rely on the referential transparency of thunk evaluation.
In the latter case, you have a proof obligation to the compiler that your API does not expose the difference between these two values. But in Haskell, you have no way of convincing the compiler that you fulfilled that proof obligation! (At least, I don't see any obvious one. Maybe a clever abuse of parametricity helps.) It might be an option in Agda, though.
In that light, it is entirely reasonable that you have to use unsafePerformIO .
Yes, of course. But as works like 'amb' demonstrate, we can build higher-level APIs that are unsafe under the hood, but when used as abstractions fulfill referential transparency (or, in the case of 'amb', fulfill referential transparency as long as some not-as-onerous properties are achieved.) So if you implement a reusable mechanism that does unsafe stuff under the hood, but provides all the right guarantees as long as you don't peek inside, I think that's a good step. Cheers, Edward