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

From: Stephen Chang (stchang at ccs.neu.edu)
Date: Sun Feb 5 17:11:21 EST 2012

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

Posted on the dev mailing list.