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

On Tue, Aug 14, 2012 at 10:45 AM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:
> On 2012-08-14 10:26:14 -0500, Robby Findler wrote:
>>  -----------------
>>  Γ ⊦ (error t) : t
>
> That's what I meant. It's not so bad here, but it's more awkward in
> other cases:
>
>            Γ ⊦ ctc : (con t_1)
> ------------------------------------------- TConPrompt
> Γ ⊦ (prompt/c ctc) : (con (prompt t_1 t_2))
>
> which has to look like
>
>            Γ ⊦ 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?

Yeah, I think that's the best option (but I like to see Redex being used....)

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?

Robby