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. > > Also, how can we typeset L? Should it look like some combination of > the typesetting of L1 and L2? (This part actually doable, altho not > trivial.) But if the union language actually extends some of the > non-terminals (using the part I added that you didn't request), then > the typesetting won't work out well, for the same reason that when > using the four-period ellipsis in a define-extended-language you still > see that ellipsis in the typeset version. So at a minimum, I would > like to kill that extension. I think no one will typeset the union language; it will just be created to be the language of the relevant metafunctions. > > But I would also like to hear your opinions on how something like the > above would typeset well. > > I would like to point out that if all of these non-terminals were > already in the same language, perhaps with some prefix, then there is > no typesetting issue and Redex already supports this well. The > problems all come in because we are adding lots of machinery to the > Racket<->Redex bridge and not in the Redex part itself. > > Robby > > On Mon, Feb 6, 2012 at 8:53 AM, Matthias Felleisen <matth...@ccs.neu.edu> > wrote: >> >> I have just read a dissertation with something like this. The type setting >> used all bold for one language and plain font for the other. Hard to read >> but you could figure it out. The grammar, however, used annotated >> nonterminals. >> >> The experience suggests that doing this plainly is a bad experience for the >> reader. >> >> But at the same time, it would be nice to have a mechanical way to union two >> existing languages in a tagged manner (disjoint union): >> >> (define-language-union L = (Lambda #:tag L1) (CPS #:tag L2)) >> >> It would then be possible to write contracts such as >> >> (define-metafunction L >> translate : e.L1 -> e.L2 >> ...) >> >> >> >> >> >> >> On Feb 6, 2012, at 7:59 AM, Robby Findler wrote: >> >>> How will you disambiguate them on the printed page for readers of your >>> paper? >>> >>> Robby >>> >>> On Sun, Feb 5, 2012 at 9:36 PM, Neil Toronto <neil.toro...@gmail.com> wrote: >>>> I think in my case I actually do want the same nonterminal names. The >>>> higher-order language has lambdas while the first-order language doesn't. >>>> The first-order language has an outer `let' while the higher-order language >>>> has no `let'. Every other kind of expression is the same and has the same >>>> reduction rules in each language. >>>> >>>> Neil ⊥ >>>> >>>> >>>> On 02/05/2012 03:58 PM, Robby Findler wrote: >>>>> >>>>> Yes, you guys are right-- this is not supported. You'd have to put >>>>> everything into a single language to make it work. >>>>> >>>>> I've shied away from this because it seems overly complicated, but >>>>> also because the language names ("L1" and "L2" in Stephen's example) >>>>> don't show up anywhere in the typeset version of the model. So in >>>>> order to really be clear, you want to have different non-terminals >>>>> anyway, and then it seems like putting things into the same language >>>>> is not problematic. >>>>> >>>>> But if you have some more context in the example that suggests my >>>>> reasoning is flawed, I'd love to hear it. >>>>> >>>>> Robby >>>>> >>>>> On Sun, Feb 5, 2012 at 4:46 PM, Neil Toronto<neil.toro...@gmail.com> >>>>> wrote: >>>>>> >>>>>> On 02/05/2012 03:11 PM, Stephen Chang wrote: >>>>>>> >>>>>>> >>>>>>> I want to write a redex metafunction contract that goes between two >>>>>>> languages. Is there currently a way to do this? >>>>>>> >>>>>>> For example, >>>>>>> >>>>>>> #lang racket >>>>>>> (require redex) >>>>>>> >>>>>>> (define-language L1 >>>>>>> (e 1)) >>>>>>> (define-language L2 >>>>>>> (f 2)) >>>>>>> (define-metafunction L1 >>>>>>> L1->L2 : e -> f >>>>>>> [(L1->L2 1) 2]) >>>>>>> >>>>>>>> (term (L1->L2 1)) >>>>>>> >>>>>>> >>>>>>> . . ..\..\plt\collects\redex\private\error.rkt:3:0: L1->L2: codomain >>>>>>> test failed for 2, call was (L1->L2 1) >>>>>>> >>>>>>> Switching the metafunction language to L2 similarly produces an error >>>>>>> about the domain. Currently it seems like I can't use a contract with >>>>>>> these kinds of metafunctions. How difficult would it be to support >>>>>>> this functionality? It seems like this use case should be pretty >>>>>>> common. >>>>>>> >>>>>>> I'm imagining something like: >>>>>>> >>>>>>> (define-metafunction >>>>>>> L1->L2 : L1:e -> L2:f >>>>>>> [(L1->L2 1) 2]) >>>>>> >>>>>> >>>>>> >>>>>> I'd like to know this myself. I'll be transforming terms from a >>>>>> higher-order >>>>>> language to a first-order one via closure conversion. Neither language is >>>>>> an >>>>>> extension of the other, so I can't use `defined-extended-language'. The >>>>>> only >>>>>> way I've thought of so far is to make a third language that is a superset >>>>>> of >>>>>> both. >>>>>> >>>>>> Neil ⊥ >>>>>> >>>>>> _________________________ >>>>>> Racket Developers list: >>>>>> http://lists.racket-lang.org/dev >>>> >>>> >>> >>> _________________________ >>> Racket Developers list: >>> http://lists.racket-lang.org/dev >> > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev -- sam th sa...@ccs.neu.edu _________________________ Racket Developers list: http://lists.racket-lang.org/dev
