[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 ⊥