[rust-dev] Eliminating Bounds checks on arrays

[Bennie Kloosteman]

Does Rust have bounds checking on arrays ?  I was on the bitc list and
Shap suggested rather than javas complicated ( and expensive from an
engineering point of view) bounds checking elimination in a Haskell
typesystem you can use a Natural number 1:N kind for the length.
This is a really cool technique , it makes the type system pick up the
bounds checks.

Here is Wren description ...
"
Consider the type of vectors of fixed length, where the length is
annotated in the type:

    Vec : Nat -> Type -> Type

So (Vec N A) is the type of length-N vectors with elements of type A. Now,
in addition we must have some canonical finite sets. We will also annotate
the size of these finite sets in their type:

    Fin : Nat -> Type

where (Fin n) denotes the set of all natural numbers smaller than n. Now,
indexing into these vectors does not need any dynamic bounds checks at
all. Just use the following function for indexing:

    (!) : forall n a. Vec n a -> Fin n -> a

If the following expression is well-typed,

    x!i

Then we know,

    exists (a : Type)
    exists (n : Nat)
    x : Vec n a
    i : Fin n

Which means we also know that,

    0 <= fromFin i < n

where fromFin is the natural embedding of any Fin type into regular
nats/ints. Therefore, after type checking, the dynamic value of i must be
in bounds for x.


You can play this trick to a limited extent in any language with a
sufficiently interesting type system. But in order to really get mileage
out of it, you're going to want things like addition and multiplication at
the type level. Also, you're going to want to group all the type-level
numbers together into a Nat kind, in order to rule out nonsense like (Vec
Int A).

--
Live well,
~wren

"