On Tue, Feb 7, 2012 at 12:24 PM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu> wrote: > On Tue, Feb 7, 2012 at 12:18 PM, Robby Findler > <ro...@eecs.northwestern.edu> wrote: >> On Tue, Feb 7, 2012 at 10:21 AM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu> >> wrote: >>> On Mon, Feb 6, 2012 at 9:18 PM, Robby Findler >>> <ro...@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 _________________________ Racket Developers list: http://lists.racket-lang.org/dev