[Agda] Sharing --- Q-combinators

[Peter Divianszky]

On 11/10/2012 00:11, Andreas Abel wrote:
>
>
> On 10.10.12 10:02 PM, Peter Divianszky wrote:
>> On 10/10/2012 17:15, Andreas Abel wrote:
>>> On 10.10.2012 16:42, Wolfram Kahl wrote:
>
>>>> 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.
>
> Peter, what do you mean by this syntax "r { x = y }"? Looks like a
> record update to me, but then you should have said "if (x r) and y point
> to the same...location".
>

Yes, you are right.
Given this optimization, lots of sharing would be saved and the 
programmer should not use any trick just use more record updates.
Maybe one should ask for this at the GHC mailing list.