[racket] [typed racket] type case

On Sun, Oct 23, 2011 at 11:03 AM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> So this seems the good way to go.
>
> However, of course, this does not work if the return type is compatible with Void:
>
> (: f ((U String Integer) -> Any))
> (define (f x)
>  (cond
>    [(string? x) (string=? x "hi")]
>    [(exact-nonnegative-integer? x) (= x 7)]))
>
> typechecks.
>
> I wonder if there a trick to make this work in all cases.
> Probably not with standard `cond', because as Ian suggested, this would require to specify an else clause that returns something which is not a subtype of Any.
>
> I guess you could include a type Invalid, which is NOT a subtype of Any. That would make it possible to provide a special `cond' form for which the proposed pattern would work (the else clause would be typed as Invalid). Would something like that work?

Yes, I have planned to do this for a while.  Probably the form it will
take will be a macro that always produces a type error when checked,
rather than a new type.  Then macros could use this form to ensure
exhaustiveness.
-- 
sam th
samth at ccs.neu.edu