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

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
>