title: PLT Redex: parameterizing a language definition
body: <p>This is a problem that's been nagging at me for some time, and I wonder if anyone here can help.</p>
  
  <p>I have a PLT Redex model of a language called lambdaLVar that is more or less a garden-variety untyped lambda calculus, but extended with a store containing "lattice variables", or LVars.  An LVar is a variable whose value can only increase over time, where the meaning of "increase" is given by a partially ordered set (aka a lattice) that the user of the language specifies.  Therefore lambdaLVar is really a family of languages -- instantiate it with one lattice and you get one language; with a different lattice, and you get another.  You can take a look at the code <a href="https://github.com/iu-parfunc/lvars/tree/master/redex" rel="noreferrer">here</a>; the important stuff is in <a href="https://github.com/iu-parfunc/lvars/blob/master/redex/lambdaLVar.rkt" rel="noreferrer">lambdaLVar.rkt</a>.</p>
  
  <p>In the on-paper definition of lambdaLVar, the language definition is parameterized by that user-specified lattice.  For a long time, I've wanted to do the same kind of parameterization in the Redex model, but so far, I haven't been able to figure out how. Part of the trouble is that the <em>grammar</em> of the language depends on how the user instantiates the lattice: elements of the lattice become terminals in the grammar.  I don't know how to express a grammar in Redex that is abstract over the lattice.</p>
  
  <p>In the meantime, I tried to make lambdaLVar.rkt as modular as I could.  The language defined in that file is specialized to a particular lattice: natural numbers with <code>max</code> as the least-upper-bound (lub) operation.  (Or, equivalently, natural numbers ordered by <code>&lt;=</code>.  It's a very boring lattice.)  The only parts of the code that are specific to that lattice are the line <code>(define lub-op max)</code> near the top, and <code>natural</code> appearing in the grammar.  (There's a <code>lub</code> metafunction that is defined in terms of the user-specified <code>lub-op</code> function.  The latter is just a Racket function, so <code>lub</code> has to escape out to Racket to call <code>lub-op</code>.)</p>
  
  <p>Barring the ability to actually specify lambdaLVar in a way that is abstract over the choice of lattice, it seems like I ought to be able to write a version of lambdaLVar with the most bare-bones of lattices -- just Bot and Top elements, where Bot &lt;= Top -- and then use <code>define-extended-language</code> to add more stuff.  For instance, I could define a language called lambdaLVar-nats that is specialized to the naturals lattice I described:</p>
  
  <pre><code>;; Grammar for elements of a lattice of natural numbers.
  (define-extended-language lambdaLVar-nats
    lambdaLVar
    (StoreVal .... ;; Extend the original language
              natural))
  
  ;; All we have to specify is the lub operation; leq is implicitly &lt;=
  (define-metafunction/extension lub lambdaLVar-nats
    lub-nats : d d -&gt; d
    [(lub-nats d_1 d_2) ,(max (term d_1) (term d_2))])
  </code></pre>
  
  <p>Then, to replace the two reduction relations <code>slow-rr</code> and <code>fast-rr</code> that I had for lambdaLVar, I could define a couple of wrappers:</p>
  
  <pre><code>(define nats-slow-rr
    (extend-reduction-relation slow-rr
                               lambdaLVar-nats))
  
  (define nats-fast-rr
    (extend-reduction-relation fast-rr
                               lambdaLVar-nats))
  </code></pre>
  
  <p>My understanding from the documentation on <code>extend-reduction-relation</code> is that it should reinterpret the rules in <code>slow-rr</code> and <code>fast-rr</code>, but using lambdaLVar-nats.  Putting all this together, I tried running the test suite that I had with one of the new, extended reduction relations:</p>
  
  <pre><code>&gt; (program-test-suite nats-slow-rr)
  </code></pre>
  
  <p>The first thing I get is a contract violation complaint: <code>small-step-base: input (((l 3)) new) at position 1 does not match its contract</code>.  The contract line of small-step-base is just <code>#:contract (small-step-base Config Config)</code>, where <code>Config</code> is a grammar nonterminal that has a new meaning if reinterpreted under lambdaLVar-nats than it did under lambdaLVar, because of the specific lattice stuff.  As an experiment, I got rid of the contracts on<code>small-step-base</code> and <code>small-step-slow</code>.</p>
  
  <p>I was then able to actually run my 19 test programs, but 10 of them fail.  Perhaps unsurprisingly, all the ones that fail are programs that use natural-number-valued LVars in some way.  (The rest are "pure" programs that don't interact with the store of LVars at all.)  So, the tests that fail are exactly the ones that use the extended grammar.</p>
  
  <p>So I kept following the rabbit hole, and it seems like Redex wants me to extend all of the existing judgment forms and metafunctions to be associated with lambdaLVar-nats rather than lambdaLVar.  That makes sense, and it seems to work OK for judgment forms as far as I can tell, but with metafunctions I get into trouble: I want the new metafunction to overload the old one of the same name (because existing judgment forms are using it) and there doesn't seem to be a way to do that.  If I have to rename the metafunctions, it defeats the purpose, because I'll have to write whole new judgment forms anyway.  I suppose that what I want is a sort of late binding of metafunction calls!</p>
  
  <p><strong>My question in a nutshell:</strong> Is there any way in Redex to parameterize the definition of a language in the way I want, or to extend the definition of a language in a way that will do what I want?  Will I end up just having to write Redex-generating macros?</p>
  
  <p>Thanks for reading!</p>