[Agda] Sharing --- Q-combinators

[Andreas Abel]

On 11.10.12 10:12 AM, Peter Divianszky wrote:
> 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.

Depending on how record updates are implemented, this could be easy or 
hard to change in GHC.  Looking at the emitted core should give a hint...

If you ask at the GHC list, please CC me.

Andreas

-- 
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/