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.
