[CakeML-dev] Array library

Scott Owens S.A.Owens at kent.ac.uk
Wed Apr 12 15:44:07 UTC 2017

At the moment we define Array.fromList and Array.tabulate as follows, which is operationally correct, but the type inferencer gives them types that are too specific: int list -> int array and int -> (int -> int) -> int array.

  fun fromList l =
    let val arr = array (List.length l) 0
      fun f l i =
       case l of
          [] => arr
        | (h::t) => (update arr i h; f t (i + 1))
    in f l 0 end

 fun tabulate n f =
    let val arr = array n 0
      fun u x =
        if x = n then arr
        else (update arr x (f x); u (x + 1))
      u 0

This is because of the initialisation of the array to 0, before overwriting all of the 0s with the real values. Now I can update the code to initialise the array with one of the values that will go into the array (the head of the list, and f 0, for example). However, this is not possible for fromList [] and tabulate 0, which both produce empty arrays, and the type of the contents are not constrained. I can see several ways to fix this, but none are great.

- Make fromList and tabulate be primitives in the source semantics (which could be implemented in source_to_mod rather than a later phase).
- Add a new array_empty primitive with type unit -> ‘a array
- Make an attempt to create an empty array raise an exception

Any preferences?


More information about the Developers mailing list