[racket] [typed racket] type case

If it is only for type coverage, theb why not name it as such?  There
will probably be other kinds of errors in the future.

On 2011-10-25, Sam Tobin-Hochstadt <samth at ccs.neu.edu> wrote:
> 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
>
> _________________________________________________
>   For list-related administrative tasks:
>   http://lists.racket-lang.org/listinfo/users
>


-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                  http://www.barzilay.org/                 Maze is Life!