[Agda] Sharing --- Q-combinators

[Andreas Abel]

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".

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/