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

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.

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.

-- 
sam th
samth at ccs.neu.edu