[racket] [typed racket] type case

To come back on this: I understand that Typed Racket's prime objective is that the type system should adapt to existing programming idioms as much as possible. But does this prevent new type-related idioms to be used? 

In that sense, union types are a particularly good example. They are necessary to support the kind of patterns found in previously-untyped code. But if I'm writing typed code, and I'm using union types, then I'd expect a case construct based on the type. Sure enough, this won't be code for which I could just "remove the types". 

Or is the Typed Racket philosophy definitely opposed to introducing such type-only constructs?

Thanks,

-- Éric


On Oct 20, 2011, at 3:39 PM, Sam Tobin-Hochstadt wrote:

> 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.
> 
> 2. For the particular case of the PLAI `cases' form, Eli and I have
> built something for his class which uses Typed Racket, but the
> exhaustiveness checking is done by `cases' itself.  Lots more about
> that is available from Eli's class web page [1], and I'm sure he'd be
> happy to give you the code.
> 
> [1] http://pl.barzilay.org/
> 
> On Thu, Oct 20, 2011 at 10:48 AM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
>> Hi again,
>> 
>> Is there a mechanism to do an exhaustive type case?
>> 
>> I know I can use (cond [(type-pred? v) ...]
>>                       [...])
>> 
>> but of course I have no guarantee that I am exhaustive (and of course, doing pattern matching to destruct the value would be even nicer).
>> 
>> Basically, I guess I'm after the typed version of PLAI's type-case.
>> 
>> Thanks,
>> 
>> -- Éric
>> 
>> 
>> 
>> _________________________________________________
>>  For list-related administrative tasks:
>>  http://lists.racket-lang.org/listinfo/users
>> 
> 
> 
> 
> -- 
> sam th
> samth at ccs.neu.edu
>