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

Just now, Matthias Felleisen wrote:
> 
> On Sep 22, 2012, at 10:52 AM, Eli Barzilay wrote:
> 
> > I'm not following that...  If you're saying that the two
> > constructors are not separate, then I'm more than agreeing -- I'm
> > saying that this is the main feature of the whole thing: the fact
> > that you cannot treat them as separate constructors as far as the
> > type system goes.
> 
> Correct. In ML/standard type terminology, This and That types (I
> meant types) are VARIANTS not types.

(Yes, and I use "variants" too with students -- I had to work hard to
avoid them showing up as types too, which would confuse students.)


> It is only in TR's set-oriented type system, that they can play the
> role of types too.

Obviously.


> If you wanted to use define-type in plain TR programs (not '311'),
> you'd want to expose THIS and THAT.

OK, so I think that we're saying the same thing as far as the course
context goes.  That, I think, is enough of a motivation to have such a
feature.

In a plain TR code context, I could rely on `match' to throw a type
error when I write:

  (: foo : SOMETHING -> Integer)
  (define (foo something)
    (match something
      [(This x) ...]))

This is assuming some variation of `match' that doesn't abort with an
error when it fails -- and I think that this is something that makes
much more sense in TR.  IOW, I think that it's better to make `match'
in TR throw a type error if the implicit error-throwing code is
reachable.

But I also see how I would use the feature for plain TR code too --
cases where I want to tell TR "I never want to allow code that can
handle only `This' without using `That'".  Maybe a different way to
phrase this is that this is a restriction that becomes part of my
public (TR) API, and I see a value in allowing me to make that
restriction.


[You might think that I could apply the same argument for
`Positive-Integer-Not-Fixnum' -- but there the situation is that the
type is "more hidden" since it's an implementation detail that Vincent
doesn't want to leak out, so even doing some `cases'-like thing with
it is forbidden.]

-- 
          ((lambda (x) (x x)) (lambda (x) (x x)))          Eli Barzilay:
                    http://barzilay.org/                   Maze is Life!