[racket-dev] Disjoint unions (from PR 13131)
[This is unrelated to the PR, so redirected here.] Yesterday, Vincent St-Amour wrote: Types like `Positive-Integer-Not-Fixnum' are used internally as building blocks for numeric types, but are not exported. IMO, these types wouldn't be very useful to users because - They're not used directly in the standard library (so using them wouldn't make types any more precise). - They don't correspond to very useful sets. - The set of numeric types TR provides is already somewhat overwhelming. These types aren't shown by TR's regular printer, so they're not usually a problem. However, as you point out, they still show up in some places, which is a problem. TR's printer is smart about unions that have names (such as `Integer') and displays them opaquely. `:type' exists specifically to peer inside these unions. Special-casing these internal types in `:type' (to avoid displaying them) could work, but it's not clear whether it's the right thing to do or not. This whole thing sounds similar to what I think is needed to make something like the disjoint union thing I use in my class available in TR. The thing that I think can work is (using my pl syntax) for this: (define-type SOMETHING [This Integer] [That String String]) to define two structs for `This' and `That', with constructors that accept the specified number and type of arguments, and it also defines `SOMETHING' as (U This That). There's some additional syntax-level information that makes it possible to do something like: (: foo : SOMETHING - Integer) (define (foo something) (cases something [(This n) n] [(That s t) (+ (string-length s) (string-length t))])) and complain if there's incomplete coverage or unreachable cases. (And this functionality might be possible to implement with a `match' if it's smart enough -- something that I always wished I could do, to avoid the confusion between the two. I didn't look into it, but this might be possible using the new thing that Sam added recently, where I'd add a last `_' clause with some raise a typecheck error if you can get here.) In any case, the main thing here is that `This' and `That' are available as constructors, but the corresponding types are *not* available. This means that you cannot write code that handles just `This', you must always deal with the whole `SOMETHING'. This is an intentional restriction, which makes some forms of hacking easier since it forces you to deal with these complete types -- and it happens that this kind of hacking is very common in PLAI-like classes. (Together with `cases', it makes a language feature that makes it as natural to write such code as it is in ML/Haskell.) -- ((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
Re: [racket-dev] Disjoint unions (from PR 13131)
I consider this problem distinct from Vincent's. I'd argue that the separate this/that constructors exist in your mind only. On Sep 22, 2012, at 7:23 AM, Eli Barzilay wrote: [This is unrelated to the PR, so redirected here.] Yesterday, Vincent St-Amour wrote: Types like `Positive-Integer-Not-Fixnum' are used internally as building blocks for numeric types, but are not exported. IMO, these types wouldn't be very useful to users because - They're not used directly in the standard library (so using them wouldn't make types any more precise). - They don't correspond to very useful sets. - The set of numeric types TR provides is already somewhat overwhelming. These types aren't shown by TR's regular printer, so they're not usually a problem. However, as you point out, they still show up in some places, which is a problem. TR's printer is smart about unions that have names (such as `Integer') and displays them opaquely. `:type' exists specifically to peer inside these unions. Special-casing these internal types in `:type' (to avoid displaying them) could work, but it's not clear whether it's the right thing to do or not. This whole thing sounds similar to what I think is needed to make something like the disjoint union thing I use in my class available in TR. The thing that I think can work is (using my pl syntax) for this: (define-type SOMETHING [This Integer] [That String String]) to define two structs for `This' and `That', with constructors that accept the specified number and type of arguments, and it also defines `SOMETHING' as (U This That). There's some additional syntax-level information that makes it possible to do something like: (: foo : SOMETHING - Integer) (define (foo something) (cases something [(This n) n] [(That s t) (+ (string-length s) (string-length t))])) and complain if there's incomplete coverage or unreachable cases. (And this functionality might be possible to implement with a `match' if it's smart enough -- something that I always wished I could do, to avoid the confusion between the two. I didn't look into it, but this might be possible using the new thing that Sam added recently, where I'd add a last `_' clause with some raise a typecheck error if you can get here.) In any case, the main thing here is that `This' and `That' are available as constructors, but the corresponding types are *not* available. This means that you cannot write code that handles just `This', you must always deal with the whole `SOMETHING'. This is an intentional restriction, which makes some forms of hacking easier since it forces you to deal with these complete types -- and it happens that this kind of hacking is very common in PLAI-like classes. (Together with `cases', it makes a language feature that makes it as natural to write such code as it is in ML/Haskell.) -- ((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 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [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! _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Disjoint unions (from PR 13131)
On Sep 22, 2012, at 10:52 AM, 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. Correct. In ML/standard type terminology, This and That types (I meant types) are VARIANTS not types. It is only in TR's set-oriented type system, that they can play the role of types too. If you wanted to use define-type in plain TR programs (not '311'), you'd want to expose THIS and THAT. _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Disjoint unions (from PR 13131)
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
Re: [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 _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [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! _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] Disjoint unions (from PR 13131)
On Sat, Sep 22, 2012 at 12:20 PM, Eli Barzilay e...@barzilay.org wrote: 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.) But you need the type `This` to be used in typechecking the expansion of `cases`, so that `This-field` selection works. -- sam th sa...@ccs.neu.edu _ Racket Developers list: http://lists.racket-lang.org/dev
