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

[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!