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

In addition to those options (or maybe this is what you meant by
option 3, but your words make it seem more drastic than it appears to
be, at least to me), you could go with what the literature does,
namely add more than one 'error', one for each type. Typeset it
something like "error" with a subscript for the type and use the rule:

 -----------------
 Γ ⊦ (error t) : t

(You could even just typeset it as "error" (dropping the subscript)
and people would understand.)

But stepping back a bit, this is one of the well-known shortcomings of
define-judgment-form. We decided to explore this point in the design
space, since it lets us keep the "it is all just (untyped) FP, but in
fancy syntax (and with a fancy pattern matcher)" aspect of Redex. I'm
not sure this is the best option, but I think that this constraint
keeps us from _really_ losing the performance battle, which seems
important if we want to work with larger models. Not that that helps
you with this specific problem.

Robby

On Tue, Aug 14, 2012 at 9:03 AM, Asumu Takikawa <asumu at ccs.neu.edu> wrote:
> Hi all,
>
> I've hit a problem with using Redex for designing type systems and
> wanted to see if anyone had any ideas for working around it.
>
> Background: Redex now offers the nice `define-judgment-form` feature for
> defining things like type rules. These judgments can specify either I or
> O (input or output) for each of the positions (e.g., type environment,
> term, type).
>
> For something like STLC's type system, you would want a judgment like (I
> I O) for environment, term, type. The type is an O because you want to
> synthesize the type for each term.
>
> This works out until you want to add something like `error` to your
> calculus. The desired rule for such a feature might be:
>
>   ---------------
>   Γ ⊦ (error) : t
>
> with an unconstrained type t for the result. This rule won't actually
> work in Redex because it doesn't accept a non-terminal as a synthesized
> type. For other reasons, setting the type to always be input will also
> not work (to see why, try writing the rule for function application).
>
> We've thought of four ways that we might work around this:
>
>   * Add a bottom type to our language and use subtyping for cases like
>     error above. This doesn't seem too bad for error, but isn't so
>     natural for other constructs.
>
>   * Re-formulate the type system as a bidirectional type system (ala the
>     Local Type Inference paper) with both I and O judgments.
>
>   * Add redundant type information to terms and use synthesis in all
>     cases. This complicates the expression grammar unnecessarily.
>
>   * Abandon Redex for typesetting and use something like Kanren or
>     Racklog for the computational part of the type system.
>
> None of the options seem great. Are there any other options for this use
> case? Are we missing anything obvious?
>
> Cheers,
> Asumu
> ____________________
>   Racket Users list:
>   http://lists.racket-lang.org/users