[racket] [typed racket] type case

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

[AFAIK, plai does not have `cases', but only `type-case'; from looking through the docs, it seems `cases' is the eopl construct, doing the same thing]

type-case works fine, but is not based on static types. It only works for a named datatype with variants:
(define (foo x)
(type-case MyStruct x
  (variant1 ...)
  (variant2 ...))

Now, with static types, I can have the following:

(: foo ((U Number String) -> Any))
(define (foo x)
(type-case x    ; <- not based on a single datatype
  (Number ...)
  (String ...)))

It makes sense only in the typed language because Number and String are static types, not variant tags. And it is possible to be exhaustive, ensuring that the case analysis covers all the parts of the union.

But I am indeed stating the obvious (that's TAPL chapter on sums), so I must be missing something...

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

That makes sense. To come back to the type-case on sums, I don't think it would complicate the interaction between typed and untyped code. It would just require to have static type information on the value that's type-cased. Here again, let me know if I'm missing something!

Thanks,

-- Éric