Re: fixed length arrays as types

[Judicael Courant <Judicael.Courant@lri.fr>]

Chris Hecker a écrit :
> 
> 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.
> 
> Something like this C++:
> 
> template <int unsigned N> class vector { float a[N]; };
> vector<3> add( vector<3> v1, vector<3> v2 );
> 
> vector<3> v3 = add(vector<3>(),vector<3>());    // works
> vector<3> v4 = add(vector<5>(),vector<3>());    // type error (note v<5>
> 
> I guess the higher level question is whether scalar constants
> can be part of the type signature like they can be in C++.

The answer is more or less, yes. And you can even do better than
scalar. Use functors (parameterized modules):

In fixedLengthArray.mli, put

module Make(X: sig val n : int end):
 sig
  type 'a t
  val get: 'a t -> int -> 'a
  val set: 'a t -> int -> 'a -> unit
  val make: 'a -> 'a t
  val create: 'a -> 'a t
  val init: (int -> 'a) -> 'a t
 end

then in fixedLengthArray.ml, put

module Make(X: sig val n : int end) =
 struct
  (* in fact, 'a t is just an abstract type implemented by
    'a array *)
  type 'a t = 'a array
  let get = Array.get
  let set = Array.set
  let make v = Array.make X.n v
  let create v = Array.create X.n v
  let init f = Array.init X.n f
 end


Then (once you have compiled them), you can use this module as follows
(I give here the transcript of the interaction with the
interactive interpreter):

# module ArrayThree = FixedLengthArray.Make(struct let n = 3 end);;
  module ArrayThree :
  sig
    type 'a t
    val get : 'a t -> int -> 'a
    val set : 'a t -> int -> 'a -> unit
    val make : 'a -> 'a t
    val create : 'a -> 'a t
    val init : (int -> 'a) -> 'a t
  end

Then 'a ArrayThree.t is the type of array of size 3:

# let a = ArrayThree.make 3.4;;
val a : float ArrayThree.t = <abstr>
# ArrayThree.get a 0;;
- : float = 3.400000
# ArrayThree.get a 1;;
- : float = 3.400000
# ArrayThree.get a 2;;
- : float = 3.400000
# ArrayThree.get a 3;;
Uncaught exception: Invalid_argument "Array.get".
# 

And you can't mix array of size 3 with any other array:

# module ArrayFive = FixedLengthArray.Make(struct let n = 3+2 end);;
module ArrayFive :
  sig
    type 'a t
    val get : 'a t -> int -> 'a
    val set : 'a t -> int -> 'a -> unit
    val make : 'a -> 'a t
    val create : 'a -> 'a t
    val init : (int -> 'a) -> 'a t
  end
# ArrayFive.get a 2;;  
This expression has type float ArrayThree.t but is here used with type
  'a ArrayFive.t
The type constructor ArrayFive.t would escape its scope

The first error message tells you (implicitely) that ArrayThree.t and
ArrayFive.t are incompatible types.

As for the second error message ("...would escape its scope"), I do not
understand it. I could not find anything relevant in the user manual nor
in the FAQ (searching for "scope").

Is it a bug or a feature of the type-checker?

Judicaël.
-- 
Judicael.Courant@lri.fr, http://www.lri.fr/~jcourant/
(+33) (0)1 69 15 64 85
"Montre moi des morceaux de ton monde, et je te montrerai le mien"
Tim, matricule #929, condamné à mort.
http://rozenn.picard.free.fr/tim.html