Vector lenght and indices contracts

[Dominik Pantůček]

Hello,

looking at vector-length[1] documentation, it returns
(exact-nonnegative-integer?). However, as far as I can tell, it returns
(fixnum?). Also for subsequent contracts in the vector's documentation
all indices are assumed to be (exact-nonnegative-integer?) but usually
it is impossible on given platform to use anything larger than (fixnum?)
in reality.

For example on 64bit platforms the (fixnum?) could store numbers from (-
(expt 2 62)) to (sub1 (expt 2 62)). Vector slots cannot be smaller than
64bits (machine-dependent pointers) which means 8 bytes = 3 bits of
address. Given 64bit (VERY theoretical) size of the address space, this
leaves the possibility of storing a single vector with (expt 2 61)
elements into the memory.

If I did not overlook anything, the contracts could be safely changed to
(fixnum?).

And yes, I found this issue while cleaning up my futures-sort[2] package
discussed a few months ago here. If I assume
(exact-nonnegative-integer?), I need to manually check for (fixnum?).
Even though it - given the information above - does not really make much
sense.


Should I open a PR?


Cheers,
Dominik


[1]
https://docs.racket-lang.org/reference/vectors.html#(def._((quote._~23~25kernel)._vector-length))
[2] https://docs.racket-lang.org/futures-sort/index.html

[George Neuner]

On 12/4/2019 11:03 AM, Dominik Pantůček wrote

> looking at vector-length[1] documentation, it returns
> (exact-nonnegative-integer?). However, as far as I can tell, it returns
> (fixnum?). Also for subsequent contracts in the vector's documentation
> all indices are assumed to be (exact-nonnegative-integer?) but usually
> it is impossible on given platform to use anything larger than (fixnum?)
> in reality

You are correct that (exact-nonnegative-integer?) doesn't limit values
to fixnum range, but the point of using it is more to exclude negative
values than to allow super large positive ones.

This question - or something substantially similar - has come up
before.  Your question is about contracts - which can be used from plain
Racket - but it is noteworthy that typed/Racket provides types for 
positive, negative, nonpositive, and nonnegative fixnums - but there are
no built-in tests for any of these, so a suitable contract or type
declaration has to be synthesized using multiple tests.

> For example on 64bit platforms the (fixnum?) could store numbers from (-
> (expt 2 62)) to (sub1 (expt 2 62)). Vector slots cannot be smaller than
> 64bits (machine-dependent pointers) which means 8 bytes = 3 bits of
> address. Given 64bit (VERY theoretical) size of the address space, this
> leaves the possibility of storing a single vector with (expt 2 61)
> elements into the memory.
>
> If I did not overlook anything, the contracts could be safely changed to
> (fixnum?).

It would be more correct to use  (and/c fixnum? (or/c zero? positive?))
to explicitly limit the value.

> And yes, I found this issue while cleaning up my futures-sort[2] package
> discussed a few months ago here. If I assume
> (exact-nonnegative-integer?), I need to manually check for (fixnum?).
> Even though it - given the information above - does not really make much
> sense.
>
>
> Should I open a PR?

I don't remember how the previous discussions went.  I'm not sure
anything ever really was resolved.

> Cheers,
> Dominik
>
>
> [1]
> https://docs.racket-lang.org/reference/vectors.html#(def._((quote._~23~25kernel)._vector-length))
> [2] https://docs.racket-lang.org/futures-sort/index.html

YMMV,
George

[Matthew Flatt]

I think it makes sense to refine the contract to guarantee a fixnum
result for `vector-length`.

This fact is currently documented in `unsafe-vetcor-length`, because
that's the layer where it has seemed sensible to talk about fixnums in
the past, but that's not where anyone would think to look. Meanwhile,
the contract for unsafe operation doesn't specify a nonnegative fixnum
as it should.

> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to racket-users...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/295427b5-9390-43b7-b7d5-cf25cce7
> fd4b%40comcast.net.

[Dominik Pantůček]

On 04. 12. 19 20:21, Matthew Flatt wrote:
> I think it makes sense to refine the contract to guarantee a fixnum
> result for `vector-length`.
>
> This fact is currently documented in `unsafe-vetcor-length`, because
> that's the layer where it has seemed sensible to talk about fixnums in
> the past, but that's not where anyone would think to look. Meanwhile,
> the contract for unsafe operation doesn't specify a nonnegative fixnum
> as it should.
>
> At Wed, 4 Dec 2019 14:07:47 -0500, George Neuner wrote:
>>
>>
>> It would be more correct to use  (and/c fixnum? (or/c zero? positive?))
>> to explicitly limit the value.

My impression is - so far - that (and/c fixnum? (or/c zero? positive?))
or (and/c fixnum? exact-nonnegative-integer?) should be the right way to
go with vector-length.

What about all the vector-ref, -set! and basically all indices
contracts? That should probably be the same.

Also updating the contracts for unsafe-vector-* seems reasonable to me.


Dominik

[Matthew Flatt]

At Wed, 4 Dec 2019 22:24:10 +0100, Dominik Pantůček wrote:
> What about all the vector-ref, -set! and basically all indices
> contracts? That should probably be the same.

I'm less enthusiastic about that change. It turns out that a non-fixnum
argument won't work for `vector-ref`, but the stronger constraint is
that the argument needs to be less than the vector's length. So, it
seems redundant in an unhelpful way to require that the argument
individually is a fixnum --- but I'm not completely sure.

[Jack Firth]

What if we had a `(vector-index/c vec)` contract combinator? It would be equivalent to `(integer-in 0 (sub1 (vector-length vec)))`.