fixed length arrays as types

fixed length arrays as types

[Chris Hecker]

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++.  Or, the related but different question is whether there's a way to differentiate between "float a[]" (or "float *a"), the variable length array type, and "float a[3]", a fixed length array type, which C++ doesn't do, but it lets you wrap the ideas in template classes which do allow you to represent this to the type system.

Chris

Re: fixed length arrays as types

[Judicael Courant]

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

Re: fixed length arrays as types

[Sven LUTHER]

On Sat, Nov 04, 2000 at 07:06:35PM -0800, Chris Hecker wrote:
> 
> 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++.  Or, the related but different question is whether there's a way to differentiate between "float a[]" (or "float *a"), the variable length array type, and "float a[3]", a fixed length array type, which C++ doesn't do, but it lets you wrap the ideas in template classes which do allow you to represent this to the type system.

Try using lists, 

Friendly,

Sven Luther

Re: fixed length arrays as types

[Brian Rogoff]

On Sat, 4 Nov 2000, Chris Hecker wrote:
> 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.

Use the module system to create an ADT which hides the implementation of
the type as an array. If you wish the ADT to be parameterized by a value,
as in C++ templates or Ada generic packages, then you'd use a functor to
generate the particular module you wish for. As always, the downside of
hiding representation is that you lose pattern matching on the ADT. 

> 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>

Here's a sketch in Ocaml. You'll have to decide how you want to do "add",
if you want to parameterize by array element type and all that

module type FixedLengthArrayType = 
  sig
    type elem
    type t
    val make : elem -> t
    val get : t -> int -> elem
    val set : t -> int -> elem -> unit
    val of_array : elem array -> t
    val to_array : t -> elem array
  end;;

module type ArrayParamsType = 
  sig 
    type t
    val initial_value : t
    val length : int 
  end;;

module FixedLengthArray(Params : ArrayParamsType) : 
    (FixedLengthArrayType with type elem = Params.t)= 
  struct 
    type elem = Params.t
    type t = elem array
    let make v = Array.make Params.length v
    let get fla i   = Array.get fla i
    let set fla i v = Array.set fla i v

    let (of_array : elem array -> t) = fun a -> 
      let _ = assert(Array.length a = Params.length) in 
      a
    let (to_array : t -> elem array) = fun fla -> fla
  end;;
 
module Arr3 = FixedLengthArray(struct 
                                 type t = float 
                                 let initial_value = 0.0 
                                 let length = 4
                               end);;

etc.

All that was much more verbose than it needed to be but I hope it was
clear.

> I guess the higher level question is whether scalar constants can be
> part of the type signature like they can be in C++.  Or, the related but
> different question is whether there's a way to differentiate between
> "float a[]" (or "float *a"), the variable length array type, and "float
> a[3]", a fixed length array type, which C++ doesn't do, but it lets you
> wrap the ideas in template classes which do allow you to represent this
> to the type system.

It's a bit different in ML (Ocaml and SML) in that you use the module
system to handle parameterization by values. 

-- Brian

Re: fixed length arrays as types

[Xavier Leroy]

> 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

Re: fixed length arrays as types

[Chris Hecker]

>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.  

I disagree about this.  It's really about type safety and strong typing.  You can catch a lot of errors if you can type the shape of the array (especially in numerical code).  Not only can you get rid of assert(size(array)==4) in every numerical function, but you can also safely get rid of runtime bounds checks in some cases (as Xi's work shows).  But, ignoring efficiency, I think the added type safety is a win.

>As a case in point, the evolution from C++ to Java
>follows this path.

I think it's clear Java is a step backwards relative to C++ in the realm of typesafety.  I don't mean to start a flame war, however.  I'm no fan of C++ either these days.

Chris

Re: fixed length arrays as types

[William Lee Irwin III]

On Wed, Nov 08, 2000 at 09:20:18AM -0800, Chris Hecker wrote:
> I disagree about this.  It's really about type safety and strong
> typing.  You can catch a lot of errors if you can type the shape of
> the array (especially in numerical code).  Not only can you get rid
> of assert(size(array)==4) in every numerical function, but you can
> also safely get rid of runtime bounds checks in some cases (as Xi's
> work shows).  But, ignoring efficiency, I think the added type safety
> is a win.

You might want to check out fISH then. It is very Caml-ish.
http://www-staff.mcs.uts.edu.au/~cbj/FISh/
Dependent ML, Cayenne, and Coq may also be of interest to you.

Cheers,
Bill
-- 
<pan2:#math> when i was a kid i behaved like a polynomial
--

Re: fixed length arrays as types

[Chris Hecker]

>You might want to check out fISH then. It is very Caml-ish.
>http://www-staff.mcs.uts.edu.au/~cbj/FISh/
>Dependent ML, Cayenne, and Coq may also be of interest to you.

The deCaml stuff seems interesting, but FISh doesn't look like it's ready for production programming.  Caml seems almost perfect for what I want to do, so of course I want them to change it to perfectly suit me!  :)

Chris

Re: fixed length arrays as types

[John Max Skaller]

Xavier Leroy wrote:

> 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.

	I'm not sure I can agree: I think the failure of
functional languages to cope with array sizes is simply
due to a lack of theory. 

	See http://www-staff.socs.uts.edu.au/~cbj.

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net