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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
