Some small improvements to your suggestions: 1) Instead of turning the cache off completely, you could just invalidate the cache when the parameter changes, i.e. write a `set-k!' function that updates the parameter and toggles the cache off and back on (I assume this will clear it out).
3) Move the escaping ellipses to the outermost `begin' form. This allows you to write the escape once instead of for each Redex ellipse. It also means the code within the macro definition looks more like the original. David On Wed, Mar 14, 2018 at 1:19 PM, google via Racket Users <[email protected]> wrote: > Hi, > > Papers often define parameterized metafunctions, reduction relations and > judgment forms, and when I model them in PLT Redex, I reach for Racket > parameters; but the resulting definitions are impure, and they invalidate > Redex’s cache. I first present three workarounds, none of which are > satisfactory, and then I propose two new Redex features that address this > issue. > > > PROBLEM > > To ground our conversation, let us consider an example: in Abstracting > Abstract Machines (AAM),¹ page 726, we find the metafunction ‘tick’, which > takes the ‘k’ first elements of the list ‘(e : t)’.² The ‘k’ in question is > not an explicit argument of ‘tick’, but an analysis-wide parameter that is > in scope and remains the same for definitions across several pages. To > capture this intent, the following is a Redex model in which ‘k’ is a Racket > parameter: > > #lang racket/base > > (require redex/reduction-semantics racket/list) > > (define k (make-parameter 0)) > > (define-language L > [e ::= any] > [t ::= [e ...]]) > > (define-metafunction L > tick : e _ _ _ t -> t > [(tick e _ _ _ t) ,(take (cons (term e) (term t)) (k))]) > > There is a problem with this definition, though, because ‘tick’ is impure—it > relies on the mutable external state of ‘k’—and Redex caches metafunction > applications: > > (term (tick a _ _ _ [])) > > '() > > (parameterize ([k 1]) > > (term (tick b _ _ _ []))) > '(b) > > (parameterize ([k 1]) > > (term (tick a _ _ _ []))) > '() > > The first two interactions illustrate the desired behavior: on the first, > the ‘a’ is discarded because it overflows the default maximum list size ‘k = > 0’; on the second, we bump ‘k = 1’ and ‘tick’ returns the list containing > ‘b’. But things go wrong in the third interaction, when we try again to add > ‘a’ to the empty list, this time with ‘k = 1’: Redex has cached the previous > answer, so ‘tick’ wrongly discards ‘a’. > > > WORKAROUNDS > > Workaround 1: Disable the Cache > > We set ‘caching-enabled? = #f’ whenever we parameterize ‘k’. This > deteriorates performance. > > > Workaround 2: Thread the Parameter > > Don’t have ‘k’ as a Racket parameter, and modify every definition to > propagate ‘k’ as an argument. This clutters the model and sets it apart from > the version on the paper. > > > Workaround 3: Use a macro > > #lang racket/base > > (require (for-syntax racket/base racket/syntax) syntax/parse/define > redex/reduction-semantics racket/list syntax/parse/define) > > (define-syntax-parser analysis > [(_ k:integer) > (with-syntax ([L (format-id #'k "L~a" (syntax-e #'k))] > [tick (format-id #'k "tick~a" (syntax-e #'k))]) > #'(begin > (define-language L > [e ::= any] > [t ::= [e (... ...)]]) > > (define-metafunction L > tick : e _ _ _ t -> t > [(tick e _ _ _ t) ,(take (cons (term e) (term t)) k)])))]) > > We can instantiate different analyses for our choice of ‘k’: > > (analysis 0) > (analysis 1) > (term (tick0 a _ _ _ [])) > > '() > > (term (tick1 b _ _ _ [])) > > '(b) > > (term (tick1 a _ _ _ [])) > > '(a) > > This has many issues: it is harder to read and write; it requires escaping > ellipses (see ‘(... ...)’ above); it binds the name ‘k’ in all contexts, > including undesirable ones, for example, ‘(term k)’; it may break > typesetting; it insists that ‘k’ is a literal number, not an expression that > evaluates to a number; and it may be bad for compilation performance. Some > of these issues are solved by writing even more incantations, but not all. > > > SOLUTIONS > > Currently, I’m using Workaround 1, disabling the cache, but I wish for a > lighter hammer. The simplest thing that comes to mind is a way for me to > flush Redex’s cache when I parameterize ‘k’. This would be a good > compromise: I’d still write a simple and correct model, and I’d leverage at > least some of the performance benefits of caching. Unfortunately, cache > invalidation continues to be one of the *hard problems* in computer science. > I tried to disable and reenable the cache. I tried to ‘set-cache-size!’ to a > low number and then back again. Nothing worked. > > Going further, we could introduce a ‘define-metaparameter’ form to Redex. A > metaparameter is parameterizeable like a Racket parameter, but we can use it > like a regular term in Redex definitions and the cache is aware of it. > > > * * * > > Thoughts are appreciated. Is there a better way to accomplish my goal? Is it > a valid thing to want in the first place? > > Parametrically confused, > Leandro. > > > * * * > > ¹ Van horn, David, and Matthew Might. 2012. “Systematic Abstraction of > Abstract Machines.” J. Funct. Program. 22 (4–5): 705–746. > https://doi.org/10.1017/S0956796812000238. > > ² Similar to ‘take’ from ‘racket/list’. > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
