[racket] [typed racket] type case

On Fri, Oct 21, 2011 at 12:44 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> 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".

What would such a construct look like?  Forms like `cases' from PLAI
work fine in plain Racket.

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

Some features are definitely typed-language only, such as
automatically introducing numeric coercions a la C, or type class
dispatch on the annotated return type in Haskell, or static method
resolution in Java.  I don't currently plan on adding features like
this, in large part because it would greatly complicate the
interaction between typed and untyped programs.    Instead, I think
Typed Racket should work with the Racket numeric tower, struct
properties, and the Racket class system.  So far, I haven't seen any
strong reasons why Typed Racket would need to take a different
approach.

>
> 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
>>
>
>



-- 
sam th
samth at ccs.neu.edu