[Agda] Sharing --- Q-combinators

[Wolfram Kahl]

On the code sprint page of the AIM that just finished, I read:

 |  Sharing (call by need)
 |      UN, NP, NAD, DG, AA, MT
 | [...]
 | * Day 7: If you check syntactic equality before unification, you
 |   actually gain surprisingly much. (Saves maybe 10% in the std. library
 |   typechecking time). We 've identified that De Bruijn indices are messing
 |   up sharing. Annoying! What can we do? Maybe explicit substitutions;
 |   Maybe keep track of closed terms (so substituting in a closed term is
 |   a noop and keeps sharing). We are going to run more experiments.

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


Wolfram