[Agda] Sharing --- Q-combinators

[Andreas Abel]

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

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