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

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 ⊥