[Haskell-cafe] More ideas for controlled mutation

[Edward Z. Yang]

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