[racket-dev] redex metafunction contract for two separate languages?

From: Robby Findler (robby at eecs.northwestern.edu)
Date: Tue Feb 7 13:28:16 EST 2012

On Tue, Feb 7, 2012 at 12:24 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> On Tue, Feb 7, 2012 at 12:18 PM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> On Tue, Feb 7, 2012 at 10:21 AM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
>>> On Mon, Feb 6, 2012 at 9:18 PM, Robby Findler
>>> <robby at eecs.northwestern.edu> wrote:
>>>> Actually, on second thought, I'm not yet sure how the typesetting is
>>>> going to go. Say you have something like this:
>>>>  (define-language L1
>>>>    (a ... somestuff ...))
>>>>  (define-metafunction L1
>>>>     f : a -> a
>>>>     [(f a) ...somestuff...])
>>>>  (define-language L2
>>>>    (a ... somedifferentstuff ...))
>>>>  (define-metafunction L2
>>>>     g : a -> a
>>>>     [(g a) ...somedifferentstuff...])
>>>>  (define-union-language L ((L1 l1) (L2 l2))) ;; l1 & l2 are prefixes
>>>>  (define-metafunction L
>>>>    h : l1.a -> l2.a
>>>>    [(h l1.a) ...])
>>>> I presume now that you intend to typeset all three metafunctions. How
>>>> should 'f' and 'g' be typeset so as to be clear which one comes from
>>>> which language?
>>> In most papers that I see, nothing other than context would
>>> disambiguate them, and that would be plenty.
>>> For example, take the following paper:
>>> http://dl.acm.org/citation.cfm?doid=1596550.1596592
>>> That paper has a large number of metafunctions between different
>>> languages, and (a) doesn't disambiguate between which language is
>>> which, and (b) avoids the problems listed here by using different
>>> non-terminal names, and all of it is fine.  I spent a lot of time with
>>> this paper, and none of these issues were confusing.  See, for
>>> example, the metafunctions on page 8.
>> Are you arguing for the status quo here? (As you know, this paper was
>> coded up in the current Redex :).
> No, I would say I'm arguing for the following.  Either:
> 1. Allow metafunctions between languages, with specification for each
> end, and an expectation that you won't use the same non-terminal name
> on both ends, in the same way that Redex doesn't prevent you from
> using `X' for all your keywords.

Defining metafunctions where the language of the domain and range are
different seems complicated to fit into the pattern matcher -- the
patterns in the cases would probabl have to be in a different language
that the right-hand sides, which seem complex.

> 2. Support `define-union-language', without worrying too much about
> its typesetting, because it would be primarily used for defining these
> metafunctions and not explicitly described in a paper.

I see. I'll think more about this option.

One other design question: would having the same non-terminal name in
both languages be allowed, or would it be some kind of
union-of-the-productions operation? (I'm guess inclined to let it be
an error so we can change that at some point in the future when we
understand better what we'd want.)


Posted on the dev mailing list.