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

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.)

Robby