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

From: Asumu Takikawa (asumu at ccs.neu.edu)
Date: Tue Aug 14 11:45:34 EDT 2012

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.


Posted on the users mailing list.