Proposal: Array Modification by higher-order Functions

[gteege]

For the development of builtin arrays (#319) I propose to support modification of boxed arrays not by take/put operations for elements, instead use higher order functions which apply a modification function to one or more elements.

A modification function has the type

(T, In) -> (T, Out)

where T is a boxed type and In and Out are arbitrary types for auxiliary data.
Additionally, a modification function must have the property that the first component of
the result is constructed from the first component of the argument by only applying take-
and put-operations and other modification functions. In C this means it returns the same
pointer (address) without deallocating and reallocating it in between.

Now, to modify a single element of an array, use an (abstract) higher-order function such as

modref: (Arr,(Idx,Modfun,In)) -> (Arr,Out)
type Modfun = (Elp, In) -> (Elp, Out)

where Arr is the type for the boxed array and Elp is the (boxed) type of pointer
to array elements (for arbitrary non-record element type El use the record type {cont: El}).
ModFun is a modification function type.

The call modref(a,(i,f,d)) invokes f on the i-th element of a with d as
auxiliary input (in C: f(&a[i],d)) and returns the modified a and the second component of
f's result. This is semantically equivalent to taking the element, storing it on the heap,
applying f to a pointer to it, removing it from the heap, and putting it back into the same
array element.

The linear type restrictions are automatically respected here, even if type In
is linear: since there cannot be sharing between a and d in the call to
modref, and a[i] is a subregion of a, there cannot be sharing between
&a[i] and d in the call to f.

As I see it, this approach has the following advantages:

• No need for array types with one (or even more) taken elements.
• The element can be modified in-place, if f respects the additional property
  of modification functions, given above.
• The approach can also be used to in-place modify embedded (unboxed) records in boxed records.
• Function modref is itself a modification function, so the approach can be iterated
  to modify parts of arbitrarily deep nested structures or multi-dimensional arrays.
• The modification function f can be fully implemented in Cogent.
• The approach can be extended to other higher-order functions which apply the modification
  function to several elements, iterating through the array, using In and Out for all
  kinds of folding and accumulating.

It seems to me that the only extension required for Cogent is a new category of types for
modification functions. For these types the refinement proof must additionally prove the
property given above, that the C function returns the same pointer.

[zilinc]

also see cogent/lib/gum/common/vector.cogent on bilby-buffer branch. modref ~ focus_vector.