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. 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 sa...@ccs.neu.edu _________________________ Racket Developers list: http://lists.racket-lang.org/dev
