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
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
