[racket] Transitively extend redex metafunctions

Thanks. Yes, I agree with everything. FWIW. I'm also glad to hear that
it works to just stick with the biggest language for now.

Also, metafunctions (and everything else) expand into functions that
accept a language (as a value at runtime) to create extensions. So the
main work is just sorting out how the module system should work (I
think it can be first-order for example) and then setting up the
expansion to pass the languages around at right points.

Robby

On Fri, Dec 7, 2012 at 7:30 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> On 12/7/12 7:49 PM, Robby Findler wrote:
>>
>> This is an excellent example of one of the reasons why we'd planned to
>> add a notion of modules to Redex. The idea being that you could group
>> a bunch of metafunctions/judgment-forms/reduction relations together
>> and then simultaneously extend the set of them to a new language.
>
>
> This would be excellent and I think is exactly what's right for the models
> I'm working on now.
>
>> Unfortunately, there isn't a way to do what you're asking at the
>> moment-- not because the underlying facility isn't there, but because
>> as you note, the helper function can't be redirected to the new one.
>>
>> Matthias recently suggested an imperative form of extension, where you
>> could mutate a function so that it now works in a large language.
>>
>> Would something like that help in your case, or would you want to keep
>> all of the different versions of these functions around?
>
>
> Hmmm.  If I could typeset things incrementally, the way I can now, I believe
> that would be fine.  (Although I can certainly imagine when it's important
> to have the functions around: suppose you want to prove a theorem about some
> relationship between a language and its extension -- you'd need both sets of
> metafunctions to test the theorem.)
>
> It sounds like the right thing for me to do in the meantime is define all of
> my metafunctions for the largest language and typeset things by selecting
> the cases for the subsets of each smaller language.
>
> By the way, a small, good example of where this problem pops up is in a
> language with expressions and statements, defined by mutual induction. If
> you have a well-formedness judgment (e.g., a typing relation), it's going to
> be in the form of two mutually recursive judgments.  If you add a new kind
> of expression or statement, the judgment can't be extended. (This is why I
> asked about local metafunctions.)
>
> David
>