Re: [racket-dev] A Const type constructor
On 07/25/2012 07:10 PM, D Herring wrote: On 07/25/2012 12:29 PM, Neil Toronto wrote: What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). In C, const is a contract on the function type, not on the parameter data type. This can be a very useful contract. Once const applies to a variable, it becomes sticky and requires an explicit (and easily searched) const_cast downgrade to become mutable again. This can be useful and quite annoying. Using const in one spot often causes a snowball effect where it must be manually propagated to other function prototypes. C++ allows certain fields to be marked as mutable, even when the containing object is const. A more dynamic language might be able to decorate the value instead of the function, or at least infer const-ness where possible? Here's a possible way to make the snowball-ness less of an issue: have a Mutable constructor instead, and make (Vectorof A) mean (Const (Vectorof A)). Of course, that would mean functions should accept (Vectorof A) and return (Mutable (Vectorof A)), unless they actually return an immutable vector Here's a better idea. Let's say we want to type `vector-sqrt'. The best way using Const would be vector-sqrt : (Const (Vectorof Number)) - (Vectorof Number) so that it could accept both kinds of vectors. If vectors were Const by default, it would be vector-sqrt : (Vectorof Number) - (Mutable (Vectorof Number)) so that its return values could be used anywhere. What if, when a `Vectorof' were in an argument position, it was Const, and when in a return position, Mutable? The obvious type would be best: vector-sqrt : (Vectorof Number) - (Vectorof Number) If a vector argument needed to be mutable, its type could be overridden: vector-set! : (All (a) (Mutable (Vectorof a)) Integer a - Void) In the extremely rare case that a function returned an immutable vector, the return type could be overridden: vector-immutable-vector : (All (a) (Vectorof a) - (Const (Vectorof a))) Making vector arguments Const by default could break existing code written in TR. I don't think a lot of code would break, though: 1. Racket is designed to discourage mutation. 2. Mutable data structures are hard to use in TR because they're not covariant, and ridiculously hard with numeric tower type parameters. 3. I found a nasty error: typed vector-ref indexes the wrong elements (often raising errors) on vectors from untyped code. I'm certain that because of this, there's no mixed typed/untyped code that uses vectors. To reiterate after my absence: I won't write a typed math/vector until using its exports in Typed Racket wouldn't be a huge friggin' PITA. To offer a carrot instead of a stick: There could be a short paper in this, titled The Case for a Clean, Correct, Covariant Const. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On Jul 31, 2012, at 1:31 PM, Neil Toronto wrote: To reiterate after my absence: I won't write a typed math/vector until using its exports in Typed Racket wouldn't be a huge friggin' PITA. Let me rephrase this ever so gently. Typed Racket has failed at least one real test for now, namely, writing a highly usable math library. I think this is a fair judgment, and you are posing the obvious, not so implied problem to the TR maintainers to fix this problem. They should thank you on their knees, especially Vincent. To offer a carrot instead of a stick: There could be a short paper in this, titled The Case for a Clean, Correct, Covariant Const. That is what I was thinking as I was reading your message. I have not encountered such a proposal/language before, and I think it could be a really neat extension of Vincent's PADL work. Perhaps the two of you should work out the details together and submit follow-up to PADL n+1. Oh never mind, D stands for declarative. So ship it to ICFP next year, functional languages do include mutation. -- Matthias smime.p7s Description: S/MIME cryptographic signature _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
At Tue, 31 Jul 2012 14:36:06 -0400, Matthias Felleisen wrote: On Jul 31, 2012, at 1:31 PM, Neil Toronto wrote: To reiterate after my absence: I won't write a typed math/vector until using its exports in Typed Racket wouldn't be a huge friggin' PITA. Let me rephrase this ever so gently. Typed Racket has failed at least one real test for now, namely, writing a highly usable math library. Agreed. The invariance of vectors is a pretty big usability problem here. I think this is a fair judgment, and you are posing the obvious, not so implied problem to the TR maintainers to fix this problem. They should thank you on their knees, especially Vincent. Yes, Sam and I should fix this. Neil: I'll study your proposal in detail, and see how we could add it (or something similar) to TR. Thanks for taking the time to write it out. I'll have a look at what Scala does, too. AFAIK, they also have invariant vectors and more than one numeric type, so they probably have similar problems. To offer a carrot instead of a stick: There could be a short paper in this, titled The Case for a Clean, Correct, Covariant Const. That is what I was thinking as I was reading your message. I have not encountered such a proposal/language before, and I think it could be a really neat extension of Vincent's PADL work. Agreed. Perhaps the two of you should work out the details together and submit follow-up to PADL n+1. Oh never mind, D stands for declarative. So ship it to ICFP next year, functional languages do include mutation. Sounds good to me. Neil: let's continue this discussion off-list. Vincent _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto neil.toro...@gmail.com wrote: After thinking about it, I don't want an Immutable-Vector type, for which v : Immutable-Vector proves (immutable? v) is #t. That would be seriously annoying to users of a vector library. What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). How exactly are these different? An immutable vector is a vector, but could be covariant, which seems like what you want. However, a mutable vector can't be treated as an immutable vector. -- sam th sa...@ccs.neu.edu _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On 07/25/2012 10:26 AM, Sam Tobin-Hochstadt wrote: On Wed, Jul 25, 2012 at 9:29 AM, Neil Toronto neil.toro...@gmail.com wrote: After thinking about it, I don't want an Immutable-Vector type, for which v : Immutable-Vector proves (immutable? v) is #t. That would be seriously annoying to users of a vector library. What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). How exactly are these different? An immutable vector is a vector, but could be covariant, which seems like what you want. However, a mutable vector can't be treated as an immutable vector. I don't want to tell Typed Racket This vector's values never change. I want to tell it Code in this scope never changes this vector's values. That's why I called it const instead of immutable. Neil ⊥ _ Racket Developers list: http://lists.racket-lang.org/dev
Re: [racket-dev] A Const type constructor
On 07/25/2012 12:29 PM, Neil Toronto wrote: What if TR had a notion of const-ness, like in C? Suppose (Vectorof A) is a subtype of (Const-Vectorof B) when A is a subtype of B, and (Const-Vectorof A) is never a subtype of (Vectorof B). In C, const is a contract on the function type, not on the parameter data type. This can be a very useful contract. Once const applies to a variable, it becomes sticky and requires an explicit (and easily searched) const_cast downgrade to become mutable again. This can be useful and quite annoying. Using const in one spot often causes a snowball effect where it must be manually propagated to other function prototypes. C++ allows certain fields to be marked as mutable, even when the containing object is const. A more dynamic language might be able to decorate the value instead of the function, or at least infer const-ness where possible? - Daniel _ Racket Developers list: http://lists.racket-lang.org/dev
