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