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

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.

>
> 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 <matthias at 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.toronto at 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.toronto at 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
samth at ccs.neu.edu