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

20 minutes ago, Vincent St-Amour wrote:
> At Sat, 22 Sep 2012 10:52:49 -0400,
> Eli Barzilay wrote:
> > 
> >   > (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.

I'm not sure what you mean by "used as type `SOMETHING'" -- I'm just
typing that expression in the REPL, and TR should use `SOMETHING' as
the type.  (And this actually works fine for me, though only for type
definitions with more than one variant.)


> [...] 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))

(Hm, I didn't think about doing that...  But it would be hard to do
that without an `apply' now.)


> 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.

That's mainly something that goes in the PR, since with my thing there
is some point in showing the hidden types.  But the similarity is how
the above translates to my case: I want a way to treat my user-defined
`SOMETHING' as opaque, and I want to hook into the typechecker a
restriction that TR would never give the hidden `This' type to
anything.  (And I think that I have that latter part, for >=2
variants.)

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