[Agda] Sharing --- Q-combinators
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?
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:
type Q a = a -> Maybe a
qtry :: Q a -> a -> a
qtry f x = maybe x id (f x)
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).
More information about the Agda