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

At Sat, 22 Sep 2012 10:52:49 -0400,
Eli Barzilay wrote:
> 
> 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))
> 
> 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)

This is not what I'm describing.

If `(This 1)' is used as type `SOMETHING', the TR printer will print the
type as `SOMETHING', and not `(U This That)'. This is what I mean when I
say that the TR printer is smart about named unions.

The introspection tool allows you to look inside `SOMETHING'

    > (:type SOMETHING)
    (U This That)

In your example, `(This 1)' is not used as type `SOMETHING'. It's just a
`This', so its type gets printed as `This'. If you want all `This's to
always be considered as `SOMETHING's, you can use a wrapper around the
constructor:

    (define (This-wrapper x) (Ann (This x) SOMETHING))

What I'm suggesting is that some unions (e.g. `Natural') be opaque even
to the introspection tool. Since there's no way to get something to
typecheck as `Positive-Integer-Not-Fixnum' (the typechecker will never
give that type to anything, it's just a trick to get more precise
intersections) showing it in `:type''s output is confusing.

Vincent