From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA23697 for caml-red; Wed, 8 Nov 2000 17:34:57 +0100 (MET)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id JAA21546 for <caml-list@pauillac.inria.fr>; Tue, 7 Nov 2000 09:42:01 +0100 (MET)
Received: from ext.lri.fr (ext.lri.fr [129.175.15.4])
	by concorde.inria.fr (8.11.1/8.10.0) with ESMTP id eA78g1b02679
	for <caml-list@inria.fr>; Tue, 7 Nov 2000 09:42:01 +0100 (MET)
Received: from pc87.lri.fr (IDENT:root@pc87 [129.175.8.106])
          by ext.lri.fr (8.9.3/jtpda-5.3.2) with ESMTP id JAA04157
          ; Tue, 7 Nov 2000 09:41:57 +0100 (MET)
Received: from lri.fr (IDENT:jcourant@localhost.localdomain [127.0.0.1])
          by pc87.lri.fr (8.9.3/jtpda-5.3.2) with ESMTP id JAA20533
          ; Tue, 7 Nov 2000 09:41:57 +0100
Message-ID: <3A07C055.16D9CAED@lri.fr>
Date: Tue, 07 Nov 2000 09:41:57 +0100
From: Judicael Courant <Judicael.Courant@lri.fr>
X-Mailer: Mozilla 4.72 [fr] (X11; U; Linux 2.2.14-5.0 i686)
X-Accept-Language: en
MIME-Version: 1.0
To: Chris Hecker <checker@d6.com>
CC: caml-list@inria.fr
Subject: Re: fixed length arrays as types
References: <4.3.2.7.2.20001104165041.00b3e370@shell16.ba.best.com>
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: 8bit
Sender: weis@pauillac.inria.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