[racket] [typed racket] type case

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?

I guess your answer will be that Any is the only type with which Void is compatible, so it is not "so much of a problem in practice".

Thanks,

-- Éric


On Oct 20, 2011, at 5:03 PM, Sam Tobin-Hochstadt wrote:

> On Thu, Oct 20, 2011 at 3:08 PM, J. Ian Johnson <ianj at ccs.neu.edu> wrote:
>> Does typed racket fail to typecheck because cond will return void on negative numbers or something more related to exhaustive checking regardless of return value?
> 
> The former.  Since there's no pattern matching in "core" Racket, it's
> not even clear what exhaustiveness would mean in that case.
> 
>> -Ian
>> ----- Original Message -----
>> From: Sam Tobin-Hochstadt <samth at ccs.neu.edu>
>> To: Eric Tanter <etanter at dcc.uchile.cl>
>> Cc: Racket Users <users at racket-lang.org>
>> Sent: Thu, 20 Oct 2011 14:39:19 -0400 (EDT)
>> Subject: Re: [racket] [typed racket] type case
>> 
>> There are basically two options here:
>> 
>> 1. If you just use `cond' with no `else', you get a type error when
>> your cases are not exhaustive. For example:
>> 
>> (: f ((U String Integer) -> Boolean))
>> (define (f x)
>>  [(string? x) (string=? x "hi")]
>>  [(exact-nonnegative-integer? x) (= x 7)])
>> 
>> This program will fail to typecheck.