[racket] [typed racket] type case

Wonderful!!!

Thanks Sam,

-- Éric


On Oct 25, 2011, at 5:17 PM, Sam Tobin-Hochstadt 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
>