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.