Edward Z. Yang wrote:
Laziness can be viewed as a form of controlled mutation, where
we overwrite a thunk with its actual value, thus only running
the code once and reaping great time benefits.
[..]
Hash tables take advantage of this fact by simply chaining together values
in a linked list if they land in the same bucket. Could we have similarly
bucketized memoization? What we want here is for a *thunk to possibly
evaluate to different values, but calls to the API be observationally
equivalent.* That is, if the only way I can inspect a dictionary list
is do a lookup, I don't care if my representation is [(1,4),(2,2)] or
[(2,2),(1,4)]. An obvious way to do this is to use unsafePerformIO to
read out an IORef stating the value currently being looked up, and
have the thunk evaluate to the pair of that key and the result. There
are some synchronization concerns, of course: ideally we would only
take out a lock on the thunk once we realize that the value doesn't
already exist in the memotable, but I don't think there's a way in GHC Haskell
to observe if a value is a thunk or not (maybe such a mechanism would be
useful?)
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. 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 .
Best regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
