On 5/24/12 5:29 AM, Bennie Kloosteman wrote:
> On Thu, May 24, 2012 at 5:20 AM, Jonathan S. Shapiro<[email protected]>
wrote:
>> The second point is telling: it is the essential reason that we cannot
>> implement efficient arrays and vectors within the language, but it also
>> presents a range of challenges for typing things like object headers from
>> the perspective of the runtime implementation.
>
> IM not sure how a NAT kind can prevent bounds checking eg if I want 3
> chars at point n how do you know with certainty that it is not out of
> bounds ? Java has mostly solved it at a great engineering cost and for
> JITS , mono for example only eliminates bounds checks if it a 0 to max
> length iteration.
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
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
