[Agda] Sharing --- Q-combinators
Andreas Abel
andreas.abel at ifi.lmu.de
Thu Oct 11 00:11:32 CEST 2012
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/
More information about the Agda
mailing list