Thanks Sam, that clears things up! -- Éric
On Oct 22, 2011, at 6:25 PM, Sam Tobin-Hochstadt wrote: > On Sat, Oct 22, 2011 at 2:20 PM, Eric Tanter <etan...@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 <etan...@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 > sa...@ccs.neu.edu > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/users
