[racket] Using Redex for type systems w/ unconstrained variables

From: Asumu Takikawa (asumu at ccs.neu.edu)
Date: Tue Aug 14 12:13:47 EDT 2012

On 2012-08-14 10:58:57 -0500, Robby Findler wrote:
> >            Γ ⊦ ctc : (con t_1)
> > ----------------------------------------------- TConPrompt
> > Γ ⊦ (prompt/c t_2 ctc) : (con (prompt t_1 t_2))
> >
> > and so on. Especially when you have multiple rules which induce these
> > extra type arguments.  Maybe this is the best option though.
> t_2 here is the type of the result of the prompt expression?

Yes, exactly, since the contract doesn't care what that is.

> What would be the alternative construct? I guess define-judgment-form
> could switch into some kind of a prolog mode if there were no #:mode
> spec. And maybe that would be good enough for your model, generally
> speaking?

That would be a nice addition, I think. It might not be pragmatic for
large models intended to closely model a real implementation, but for a
calculus (like the one I'm working on) I suspect it'd be performant


Posted on the users mailing list.