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

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

Cheers,
Asumu