[MLton] user-level elimination of array bounds checks

[Matthew Fluet]

> That's all my examples for now.  As to practicality, I'm not sure.
> Here's how I'd implement ARRAY.
>
> ------------------------------------------------------------
> structure Array:> ARRAY =
>    struct
>       type 'a t = 'a Array.array
>
>       structure Elt =
> 	 struct
> 	    datatype 'a t = T of 'a Array.array * int
> 	 end
>
>       fun elt (a, i) =
> 	 if 0 <= i andalso i < Array.length a
> 	    then SOME (Elt.T (a, i))
> 	 else NONE
>
>       structure Elt =
> 	 struct
> 	    open Elt
>
> 	    fun equals (T (_, i), T (_, i')) = i = i'

Don't you also need to check if the arrays are equal?  Otherwise, it seems
as though:
val a = Basis2002.Array.array(10,1)
val b = Basis2002.Array.array(20,2)
val SOME elt1 = Array.elt(a,5)
val SOME elt2 = Array.elt(b,5)
val b1 = Array.Elt.equals(elt1,elt2)
val b2 = Array.Elt.get(elt1) = Array.Elt.get(elt2)
would have b1 = true but b2 = false.

> 	    fun get (T (a, i)) = Array.sub (a, i)
>
> 	    fun set (T (a, i), x) = Array.update (a, i, x)

Presumably these are the Unsafe sub and updates.

> 	    fun index (T (_, i)) = i
>
> 	    fun next (T (a, i)) = elt (a, i + 1)
>
> 	    fun prev (T (a, i)) = elt (a, i - 1)

I would think that the following is just a little more efficient:

            fun next (T (a, i)) = let val j = i + 1
                                  in if j < Array.length a
                                        then SOME (T (a, j))
                                     else NONE
                                  end
            fun prev (T (a, i)) = let val j = i - 1
                                  in if 0 <= j
                                        then SOME (T (a, j))
                                     else NONE
                                  end

The point is that a value T (a, i) of type 'a Elt.t is definitely within
bounds, so we know that 0 <= i andalso i < Array.length a.  Hence, it
certainly follows that 0 <= i + 1 andalso i - 1 < Array.length a.
Actually, the real point is that if the value was created too far away,
then the optimizer won't be able to see the bounds check used to create
the value.