I consider this problem distinct from Vincent's. I'd argue that the separate this/that constructors exist in your mind only.
On Sep 22, 2012, at 7:23 AM, Eli Barzilay wrote: > [This is unrelated to the PR, so redirected here.] > > Yesterday, Vincent St-Amour wrote: >> >> Types like `Positive-Integer-Not-Fixnum' are used internally as building >> blocks for numeric types, but are not exported. >> >> IMO, these types wouldn't be very useful to users because >> - They're not used directly in the standard library (so using them >> wouldn't make types any more precise). >> - They don't correspond to very useful sets. >> - The set of numeric types TR provides is already somewhat overwhelming. >> >> These types aren't shown by TR's regular printer, so they're not usually >> a problem. >> >> However, as you point out, they still show up in some places, which is a >> problem. TR's printer is smart about unions that have names (such as >> `Integer') and displays them opaquely. `:type' exists specifically to >> peer inside these unions. Special-casing these internal types in `:type' >> (to avoid displaying them) could work, but it's not clear whether it's >> the right thing to do or not. > > This whole thing sounds similar to what I think is needed to make > something like the disjoint union thing I use in my class available in > TR. The thing that I think can work is (using my pl syntax) for this: > > (define-type SOMETHING > [This Integer] > [That String String]) > > to define two structs for `This' and `That', with constructors that > accept the specified number and type of arguments, and it also defines > `SOMETHING' as (U This That). There's some additional syntax-level > information that makes it possible to do something like: > > (: foo : SOMETHING -> Integer) > (define (foo something) > (cases something > [(This n) n] > [(That s t) (+ (string-length s) (string-length t))])) > > and complain if there's incomplete coverage or unreachable cases. > (And this functionality might be possible to implement with a `match' > if it's smart enough -- something that I always wished I could do, > to avoid the confusion between the two. I didn't look into it, but > this might be possible using the new thing that Sam added recently, > where I'd add a last `_' clause with some "raise a typecheck error if > you can get here".) > > In any case, the main thing here is that `This' and `That' are > available as constructors, but the corresponding types are *not* > available. This means that you cannot write code that handles just > `This', you must always deal with the whole `SOMETHING'. This is an > intentional restriction, which makes some forms of hacking easier > since it forces you to deal with these complete types -- and it > happens that this kind of hacking is very common in PLAI-like > classes. (Together with `cases', it makes a language feature that > makes it as natural to write such code as it is in ML/Haskell.) > > -- > ((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay: > http://barzilay.org/ Maze is Life! > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev _________________________ Racket Developers list: http://lists.racket-lang.org/dev