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 XAA14430 for caml-redist@pauillac.inria.fr; Mon, 15 May 2000 23:02:30 +0200 (MET DST)
Resent-Message-Id: <200005152102.XAA14430@pauillac.inria.fr>
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA21459 for <caml-list@pauillac.inria.fr>; Mon, 15 May 2000 19:47:32 +0200 (MET DST)
Received: from babbage.ececs.uc.edu (mail.ececs.uc.edu [129.137.8.2])
	by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e4FHlPP25899;
	Mon, 15 May 2000 19:47:26 +0200 (MET DST)
Received: from gatekeeper-internal.ececs.uc.edu (gatekeeper-internal.ececs.uc.edu [129.137.8.10])
	by babbage.ececs.uc.edu (8.9.3+Sun/8.9.3) with ESMTP id NAA06492;
	Mon, 15 May 2000 13:47:15 -0400 (EDT)
Date: Mon, 15 May 2000 13:47:15 -0400 (EDT)
From: Hongwei  Xi <hwxi@ECECS.UC.EDU>
To: Xavier Leroy <Xavier.Leroy@inria.fr>
cc: "'caml-list@inria.fr'" <caml-list@inria.fr>
Subject: Re: reference initialization
In-Reply-To: <20000515104954.52686@pauillac.inria.fr>
Message-ID: <Pine.GSO.4.21.0005151309280.9542-100000@gatekeeper.ececs.uc.edu>
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Resent-From: weis@pauillac.inria.fr
Resent-Date: Mon, 15 May 2000 23:02:30 +0200
Resent-To: caml-redist@pauillac.inria.fr

What I had in mind is actually something pretty simple (since it won't
be very useful if it is not simple :-))

> My gut feeling about this approach is that the type system could
> probably work well for arrays that are initialized linearly, e.g.
> 
>         let a = Array.create n in
>         for i = 0 to n - 1 do
>           a.(i) <- ...
>           (* at this point, the type system knows that 
>              a.(0)...a.(i-1) are initialized and
>              a.(i)...a.(n-1) are not *)
>         done
>         (* at this point, the type system knowns that all elements of a
>            are initialized *)
> 
> But notice that most of these cases are easily expressed using Array.init!

But one common case is not covered: when you initialize A[i], you may
need values stored in A[j] for some 0 <= j < i. Is it possible to make
'init' handle this case as well. I must say that I have problems writing
such a function. This is certainly a problem that people who are
interested in generic programming should study (if it has not be
studied yet).

> However, the type system is going to break horribly on more complex
> initialization patterns, e.g. the following code for tabulating the
> inverse of a permutation f over [0...n-1] :
> 
>         let a = Array.create n in
>         for i = 0 to n - 1 do a.(f(i)) <- i done
> 
> So, I don't think the (Caml) programmer will gain much from a type
> system/static analysis for array initialization.  (For a lower-level
> language such as TAL, the story may be different, though.)

In this case, I could imagine that there are programmers who 
would like to verify that this code indeed initialize every
array cell; this is clearly a case where initialization upon
allocation doesn't make much sense.

Is it possible to have something like the following in the library:

Array.init': int -> (int -> (int * 'a)) -> 'a Array

let Array.init' n f =
  let a = Array.create n in
  for i = 0 to n - 1 do
    let (j, v) = f i
    in a.(j) <- v
  done
  (* then check that all cells are initilized *)