[racket] [typed racket] type case

On Sun, Oct 23, 2011 at 1:39 PM, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
>
> 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.

This is now implemented in git.

There's an `typecheck-fail' form which raises a type error when it is
reachable. Here's an example [1]

(define-syntax (cond* stx)
  (syntax-case stx ()
    [(_ x clause ...)
     #`(cond clause ... [else (typecheck-fail #,stx "incomplete
coverage" #:covered-id x)])]))

(: f : (U String Integer) -> Boolean)
(define (f x)
  (cond* x
         [(string? x) #t]
         [(exact-nonnegative-integer? x) #f]))

This produces a type error highlighting the `cond*' form, with the message:

  Type Checker: incomplete coverage; missing coverage of Negative-Integer in:
  (cond* x ((string? x) #t) ((exact-nonnegative-integer? x) #f))

[1] https://gist.github.com/1314097
-- 
sam th
samth at ccs.neu.edu