[racket-dev] "Disjoint" unions (from PR 13131)

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