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

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?

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.

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
>