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

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