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

A few minutes ago, Matthias Felleisen wrote:
> 
> I consider this problem distinct from Vincent's. 

Yes, the problem is separate (hence moving the discussion) -- it's the
feature that he mentioned (being able to hide types) that I was
referring to.


> I'd argue that the separate this/that constructors exist in your
> mind only.

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.  Using
plain structs so there's a separate `This' and `That' types is exactly
the thing that I want to remove from these type definitions.  To make
this even more concrete, if the types are hidden, then I cannot write
this (I'm overloading `This' as both the constructor name and the type
name):

  (: foo : Integer -> This)
  (define (foo x) (This x))

because `This' is not bound as a type.  The nice feature that Vincent
describes (and that I didn't know about) is how TR will not show
hidden types without the explicit introspection tool, so even if I
leave things for TR's inference, I would see this on the REPL:

  > (This 1)
  - : SOMETHING     <--- the type is not `This'
  (This 1)

so I'm not tempted to try to use `This' as a type somewhere.

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