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

Looks like a good design, and we really want this. Thanks -- Matthias



On Feb 6, 2012, at 11:16 AM, Robby Findler wrote:

> Something like that should be straightforward to accommodate in Redex.
> I'm imagining:
> 
>  (define-union-language <new-lang-name> (<old-lang> ...)
>     (<nt> <production> ...) ...)
> 
> where
> 
>   <old-lang> ::= <id> | (<id> <prefix>)
> 
> The extra non-terminals and productions would be like a immediate
> language extension to the union'd language (and indeed, would make
> define-extended-language be a shorthand for define-union-language with
> one <old-lang> and no prefix).
> 
> If there was no prefix specified, then define-union-language would
> insist that the non-terminals do not overlap.
> 
> For the below, tho, that would mean you'd write "L1.e" not "e.L1" but
> I suppose you wouldn't object to that.
> 
> And, if you did want to typeset "L1.e" as a bold e and "L2.e" as an
> italic e, then you could probably still do that by setting up the
> appropriate rewriters (I think).
> 
> 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
>>