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

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

Robby