[racket] [typed racket] type case

On Sat, Oct 22, 2011 at 2:20 PM, Eric Tanter <etanter at dcc.uchile.cl> wrote:
> 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 ...)))

Would this behave any differently than:

(cond
  [(number? x) ...]
  [(string? x) ...])

Certainly, Typed Racket could provide a macro that encapsulated this
translation, but note that it doesn't work for plenty of cases, such
as function types.  Additionally, it will be vastly less efficient
than something like `type-case', where everything is a tagged
structure.

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

The difference is that EOPL/PLAI-style type defintions are exactly
like the sum types describe in TAPL, but Typed Racket union types are
very different.  In particular, sums have tags, whereas unions do not
have tags.  For example:

  (U (Number -> String) (String -> Number))

There are no tags in the value that distinguish one from the other.
-- 
sam th
samth at ccs.neu.edu