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

That may be doable, based on what Burke is already working on. I think
we've discussed it a little bit. (But probably not soon, I'm sorry to
say.)

Robby

On Tue, Aug 14, 2012 at 11:13 AM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:
> 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