[Agda] Sharing --- Q-combinators

Andreas Abel andreas.abel at ifi.lmu.de
Wed Oct 10 17:15:18 CEST 2012

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 


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

More information about the Agda mailing list