# [Agda] Sharing --- Q-combinators

Wolfram Kahl kahl at cas.mcmaster.ca
Wed Oct 10 16:42:18 CEST 2012

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?
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:

(and would be willing to contribute this to Agda if you find it useful).

Wolfram