[Agda] Sharing --- Q-combinators

[Peter Divianszky]

On 10/10/2012 17:15, Andreas Abel wrote:
> On 10.10.2012 16:42, Wolfram Kahl wrote:
>>
>> Have you heard of John Harrison's Q-combinators?
>> They are about sharing at the Haskell (originally ML) run-time level,
>> but could still be relevant for some aspects of this --- using them would
>> at least make substitution on closed terms keep sharing.
>>
>>
>> Central idea: Change |f : a -> a| to |f' : a -> Maybe a| returning
>>
>>    Nothing     for ``no change''
>>    Just x      for ``new value |x|''
>>
>> Then |qtry f' = f|, but |qtry f'| preserves more sharing, with:
>>
>> \begin{code}
>> type Q a = a -> Maybe a
>>
>> qtry :: Q a -> a -> a
>> qtry f x = maybe x id (f x)
>> \end{code}
>>
>>
>> I have put an old Haskell implementation of mine up at:
>>
>>     http://relmics.mcmaster.ca/~kahl/Haskell/QCombinators.lhs
>>
>> (and would be willing to contribute this to Agda if you find it useful).
>
> I'd do this with a writer monad that writes to a "dirty" bit.  If dirty
> has not been set, we can discard the function result and use the
> original value.
>
> Use of Maybe seems a bit awkward since it is more naturally an error
> monad...
>
> Andreas
>

These techniques would not be necessary if GHC would compile code which 
returns

r { x = y }

as a reference to r if x and y points to the same memory location.