[racket] Transitively extend redex metafunctions

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.

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?

Robby

On Fri, Dec 7, 2012 at 4:28 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> The various extension forms for redex are critical for code re-use, but
> extensions break down when the things (metafunctions, judgments, etc.) being
> extended are not monolithic, but instead call helper metafunctions or
> judgments.  Due to the paucity of binding forms for these things, sometimes
> separate helper metafunctions are unavoidable (e.g. if you write an
> accumulator-style metafunction, you will need two top-level definitions; you
> can't place the metafunction with the accumulator within the definition of
> the other).
>
> Here is an example that demonstrates the problem.  First a good use of
> extension:
>
> (define-language L
>   (A string))
>
> (define-metafunction L
>   f : any -> #t or #f
>   [(f A) #t]
>   [(f any) #f])
>
> (define-extended-language M L
>   (A .... number))
>
> (define-metafunction/extension f M
>   g : any -> #t or #f)
>
> (test-equal (term (g "x")) #t)
> (test-equal (term (g 7))   #t) ;; as we'd expect since 7 is an A in M
>
> Now, let's define two seemingly equivalent metafunctions, but have a call to
> a *helper* metafunction, in this case f:
>
> (define-metafunction L
>   h : any -> #t or #f
>   [(h A) (f A)]
>   [(h any) #f])
>
> (define-metafunction/extension h M
>   i : any -> #t or #f)
>
> (test-equal (term (i "x")) #t)
> (test-equal (term (i 7))   #t) ;; this fails since 7 is not an A in *L*
>
> Here the call to i re-interprets h on language M, but the call to f does no
> re-interpretation, so its using f as a metafunction of langauge L causing
> the test to fail.
>
> It seems like the right thing is to transitively re-interpret all
> metafunctions and judgments that are *used* when extending a metafunction or
> judgment.
>
> If this kind of general solution can't be supported, what would go a long
> way for me is to have the ability to locally bind helper metafunctions
> within a metafunction definition and have those be re-interpreted when the
> metafunction is re-interpreted.
>
> In other words, I'd be happy if I could write this and have it work:
>
> (define-metafunction L
>   h : any -> #t or #f
>   [(h A) (f A)]
>   [(h any) #f]
>   with
>   f : any -> #t or #f
>   [(f A) #t]
>   [(f any) #f])
>
> (define-metafunction/extension h M
>   i : any -> #t or #f)
>
> David
> ____________________
>  Racket Users list:
>  http://lists.racket-lang.org/users