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 <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
