Re: fixed length arrays as types

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> Is there any way to do this:
> type vector3 = [| float; float; float |];
> Basically, I want an array of a given length to be a given type, so
> I can use the type system to check add_vector3 rather than throwing
> if the arrays don't match.  I know I can make records {x:float,
> y:float} but I'd like it to be parameterizable at compile time.

I understand why you'd like to do this, but having array sizes in the
types, along with sufficient polymorphism over array sizes (so that a
fixed-size array can be viewed as a variable-size array whenever needed),
all in a type inference setting, would require a fairly complex type
system.  (See for instance Pfenning and Xi's Dependent ML.)

To me, having array sizes in the array types is mostly a left-over
from languages where the compiler needs to treat static or
stack-allocated arrays differently than dynamically-allocated arrays.
My feeling is that when all arrays are dynamically allocated, it's
more natural and a whole lot simpler to never reflect array sizes in
array types.  As a case in point, the evolution from C++ to Java
follows this path.

- Xavier Leroy