Array programming

[patrick-nicodemus]

It explains in the README that a goal for Koka is to support array programming better in the future, and I wanted to ask what that might look like, and what is currently possible.

1. I want to map a function f: 'a -> 'a along a vector, and have this update in place. Is this: currently achievable, an eventual design goal, probably never going to happen, etc.
2. I want to sort a vector of floating point numbers in place: is this ever going to happen?
3. I want to sort a vector of floating point numbers, not necessarily in place but by an algorithm that does not involve converting it into a list, sorting the list, and then converting the list to an array, because this seems to involve much more pointer chasing than a simple ordinary array sort and is probably much slower because of cache locality issues (although I would be very interested to hear if I'm wrong about this)

A related question I have is that, by reading your group's papers, it seems that you can use effects to control stateful computation in the same way that Haskell does with the state monad and runST.

The vectors defined in the standard library are immutable. It is not clear to me whether Koka gives the programmer a way to use scoped effects to do stateful array computations, is there anything there? The documentation for the modify function talks about in-place updates for vectors but I unfortunately did not really understand that bit.

[anfelor]

Hi @patrick-nicodemus!

1. Is fun map( v : vector<a>, f : a -> e b) : vector<b> what you had in mind? This is in-place as long as the input vector v is unique.
2. Sure, this sounds like you want an in-place quicksort?
3. Sure, there are a few algorithms for this.

The vectors defined in the standard library are immutable

Actually, they have immutable semantics, but they do update in-place if the vector is unique.
You can implement both (2) and (3) in plain Koka, making use of the destructive vector assignment:

vec[idx] := value

sets index idx of vec to be value. This changes the vector pointed to by vec, but it does not change any other vectors in your program. We ensure this by checking at runtime that the memory underlying vec is only used here: in that case we can mutate it in-place. Otherwise, we first copy the memory to ensure that no accidental mutation of other vectors occurs.

I don't think that there is any issue with our API for vectors and it should be able to do everything you want to do. However, performance might not be competitive with C++ (but likely still be good enough for your needs). We want to improve two performance aspects in the future:

• One issue with the current implementation is that we do this check everytime you write :=. This is often unnecessary, for example in a for-loop on the same vector. Then, only in the first iteration there is a risk that the vector is used elsewhere. In latter iterations we can trust that the first iteration will have done the check (and copy if necessary). However, these extra checks will prevent the program from getting vectorized, which can be an order of magnitude performance difference.
• We currently use the same memory layout for all types of elements in the vector. This is in contrast to languages like C++, which specialize vectors to the type of the element. In practice, that can lead to much better cache usage. However, adding this to Koka would be a major change and we currently don't have the bandwidth to take on this project.

I implemented a graph theory algorithm using the vector API a few years ago: https://github.com/anfelor/koka-maximum-cardinality-matching/tree/main. Performance was slower than C++ due to the issues above, but still pretty fast.

[TimWhiting]

@anfelor
That is what we should be doing with vector, however, the implementation actually copies the vector for the map api currently.

Additionally while the documentation says map uses a total function, the implementation does not match, which means the vector could be partially uninitialized (related #391, #416, #420), if an effect changes control during the map. This is a bit of uncharted territory, but in the case of exceptional control it should just deallocate fine, due to the fixes implemented for the related issues. It seems like the change in map happened long before I started working with Koka, and I don't know if it was intentional or not. In some community libraries we started experimenting with some additions to the standard library here including a vector-list<a> / aliased as vlist<a> if you want a short name, which actually takes into account the reference count, and also automatically resizes by doubling the capacity when full (more close to imperative expectations, while staying immutable in the semantics).

Also, I didn't realize that the vec[idx] := value actually copied the vector on non-unique references, just checked in the implementation and that seems to be correct. By the way it only would work on vectors that are local variables - the type is assign/@index(^self : local-var<s,vector<a>>, ^index : int, assigned : a) : <local<s>,exn|e> (). However due to #522, I do not think the reference count is actually ever unique.

In general mutable variables are currently not very performant, due to needing to keep a reference / immutable copy around in case the mutation on the right hand side could use a ctl effect. We should investigate a variant of mutable variable assignment where the rhs is restricted to linear effects so that we can use vectors (embedded in other objects - like vlist) performantly, instead of only supporting 'destructive' vector assignment on the local variable vectors.

[patrick-nicodemus]

(Edit: I hadn't had a chance to read TimWhiting's response before writing this)

Hey @anfelor, thanks for your response!
So, the source code for map in the documentation is

// Apply a total function `f` to each element in a vector `v`
pub fun map( v : vector<a>, f : a -> e b ) : e vector<b>
  val w = unsafe-vector(v.length).ssize_t
  v.foreach-indexedz fn(i,x)
    unsafe-assign(w,i,f(x))
  w

I would be interested in understanding how compiler is able to infer that this can be done in place, at a high level what is the reasoning it employs?

I will probably wait until the morning to test out the quicksort code, but that use of the word "immutable" is somewhat surprising to me. I was not aware of the destructive update operator you mention, it is not mentioned in the sample code supplied with the VSCode plugin (I grepped for it just now) and it is not in the vector file in the stdlib - https://koka-lang.github.io/koka/doc/std_core_vector.html - maybe it would be good to add it to one or both of these? (I will also point out that when I read the phrase "immutable vector", my first reaction is definitely not "This probably has a destructive update operator, and if I search through the documentation long enough, I will find it", which is another reason to mention it prominently.)

It sounds like by "immutable" you mean something like, there is a guarantee of no aliasing. So in the code

val b = a;
a[i] := some_value

the array b is unchanged and a is copied if necessary.

I am not sure I understand the reasoning behind referring to this as
"immutability."
I guess a[i] := some_value means something like,

let c = a with [i] = v

in Futhark (https://futhark-lang.org/blog/2022-06-13-uniqueness-types.html)
except that c and a have the same name, so you're introducing a new and conceptually different array a which shadows the first one, but also the update happens in-place, because if the old a is shadowed by the new a then it certainly can't be referred to again, so you might as well update it in-place.

Is this roughly correct?

[TimWhiting]

By destructive updates and immutability, we mean the following (@anfelor correct me if I'm wrong):

fun main()
  var a := vector-init-total(10, fn(i) i)
  val b = a
  a[0] := -100
  b.map(show).join(",").println
  a[1] := -200
  a.map(show).join(",").println

results in

0,1,2,3,4,5,6,7,8,9
-100,-200,2,3,4,5,6,7,8,9
// b is a copy of the original vector.
// a is updated destructively / in-place

Or at least that should be the behavior. Unfortunately I think it is not the case due to #522?

[patrick-nicodemus]

Thank you, this is clear.
Can you link to the documentation for the destructive update syntax a[i] := v or add it to the documentation if it does not exist? The idea that "a[i]" is a valid "Lvalue" is not mentioned anywhere I can find. I suggest that it should occur in the samples folder distributed with the VS plugin and in the page for vectors. https://koka-lang.github.io/koka/doc/std_core_vector.html

Further, in this documentation:
https://koka-lang.github.io/koka/doc/std_core_types-source.html#type_space_vector
I suggest to edit the comment to clarify the meaning of the word "immutable" in the sense established in this issue - i.e., "supporting destructive update"

It is my subjective opinion that "immutable, and supporting destructive update" is a contradiction in terms, and a better term would be something like "vectors providing a no-aliasing guarantee", or "alias-free vectors", because to me mutation and destructive update / destructive assignment are synonymous. I speculate that there are enough others who interpret the words the same way I do to cause confusion. However, I will not press the point if you insist on the term "immutable."

[anfelor]

That is what we should be doing with vector, however, the implementation actually copies the vector for the map api currently.

Thanks for checking, @TimWhiting! I wonder if we should rewrite the function to use in-place updates?

However due to #522, I do not think the reference count is actually ever unique.

Does that apply here? If I remember correctly, vec[i] := v is not compiled into vec := assign/@index(vec, i, v), but rather into the plain, side-effecting statement assign/@index(vec, i, v). Then the reference count should still be unique?

the source code for map in the documentation is ... I would be interested in understanding how compiler is able to infer that this can be done in place

@patrick-nicodemus, as Tim pointed out above, I wrongly assumed the function would use in-place update when the implementation does not support this yet.

So in the code ... the array b is unchanged and a is copied if necessary.

Yes, exactly! b is equal to the old copy of a, and a refers to a new array with index i set to v. I guess we could elide the copy if v is equal to the previous element at index i, but we do not do that in practice, so a will always be copied in this case.

By destructive updates and immutability, we mean the following

Thanks! That's a great explanation.

Or at least that should be the behavior.

Did you encounter an issue here? On my machine, your code returns:

0,1,2,3,4,5,6,7,8,9
-100,-200,2,3,4,5,6,7,8,9

which is what I would have expected. I don't understand why the last output line is duplicated in your output.

[TimWhiting]

@anfelor
I'd be very happy if I was wrong, I'll have to take a look at it deeper later. You probably are correct, and it probably works precisely due to the fact that if the variable is used later, the ref(which is how local state is implemented) is duped, and not the internal vector, but I know I have seen some non-unique behavior with local variables and non-vectors. (More below)

As far as the example code, I had simplified it after pasting it: The following snippet was the original, which is why the last line of the output was duplicated. I was trying to demonstrate that often we want to use a after doing several modifications - it would be useless to modify it several times and then never use it - or often we reference a itself on the rhs of the assignment (i.e. to update an element of the vector).

fun main()
  var a := vector-init-total(10, fn(i) i)
  val b = a
  a[0] := -100
  b.map(show).join(",").println
  a[1] := -200
  a.map(show).join(",").println
  val c = a
  c.map(show).join(",").println

In fact I think this is precisely the problem I was trying to illustrate:

fun main()
  var a := vector-init-total(10, fn(i) SomeRefObject(i))
  a[0] := a[0].update()

The problem is that at the point of call to update(), the vector still has an owned reference to the object, as well as the owned reference in the update function (ref count of 2 - technically 1 since Koka uses 0 as a unique reference). So although the vector can be used in place, the object stored in the vector doesn't have the same advantage. This is due to the fact that the update() or := function could yield control via an exception (index out of bound) or otherwise. Of course with integers we don't quite have the same problem, since they are mostly value types. However I'd really like a variant where we can borrow something from a vector and leave a hole (transferring ownership), (ensuring of course that the right hand side is a linear effect), and then filling the hole with the result. In particular we'd need to make sure the index is valid prior to calling the right hand side of the assignment, to ensure we don't assume uniqueness and then throw an exception.

It also looks like we have a different potential issue with the observability of destructive updates (to all local variables):

fun main()
  var a := vector-init-total(10, fn(i) i)
  val b = a
  a[0] := -100
  b.map(show).join(",").println
  with finally
    a.map(show).join(",").println
  a[2] := -1
  a[1] := a[100] + 100

This outputs:

0,1,2,3,4,5,6,7,8,9
-100,1,-1,3,4,5,6,7,8,9
uncaught exception: index out of bounds

Which as you can see shows the mutation to a[2]. Since the a captured in the finally closure is actually a local variable reference, it is immutable semantics as far as the ref goes, but since the ref encapsulates mutable state, we see mutations to the inner state. I don't know that this is actually a problem, but it does mean that if you capture a variable in a closure and want the value from that point in time / to keep a checkpoint or history, you need to explicitly dereference it prior to capturing it in the closure. I think that is to be expected for the most part. But in terms of transactional state, it does not, and would require an explicit effect. We should probably document that local vars do not have "immutable" and by that I mean transactional semantics. The variables within them do have immutable semantics though.

This is what I think @patrick-nicodemus was trying to get at: when he said there is a contradiction between: "immutable, and supporting destructive update". However, I'd push back that it isn't the vectors that are providing destructive update by themselves, it is the fact that they are using local variables which provide non-transactional state effect semantics. And also, just because the effect for local state uses non-transactional state semantics doesn't mean that it isn't "pure" or "immutable", as illustrated by the state and exn handler combination in Koka's book: https://koka-lang.github.io/koka/doc/book.html#sec-combine. All it means is that local vars have chosen an ordering for composing state and surrounding handlers which provides non-transactional semantics.

[TimWhiting]

Thanks for checking, @TimWhiting! I wonder if we should rewrite the function to use in-place updates?

We should, but due to the effect issue, we really need a way to qualify a polymorphic effect variable to be linear. I know Daan has a paper about that he did with Jonathan Brachthäuser: https://www.microsoft.com/en-us/research/publication/qualified-effect-types/, but I don't see the ability to do that in the current Koka codebase.

We could make a variant of map which is total, but that really restricts the kinds of things you can do. (Especially if you cannot dereference other local variables).

[anfelor]

In fact I think this is precisely the problem I was trying to illustrate:

Yes, that is right. You would have to write something like:

fun main()
  var a := vector-init-total(10, fn(i) SomeRefObject(i))
  val v = a[0]
  // there are now two reference pointing to the same object: a[0] = v
  a[0] := default
  // erase reference from array, making `v` unique
  a[0] := v.update()

for some default value of the correct type. It would be much nicer if we did not have to do this, but could express that the cell a[0] should be overwritten by null for a short amount of time.

It also looks like we have a different potential issue with the observability of destructive updates

Hmm, I agree that this behavior could be counter-intuitive, but for me the output is exactly what I would have expected. Conceptually, the finally runs after all computations so far, and it seems sensible to me that the local variables may have been mutated so far.

it isn't the vectors that are providing destructive update by themselves

Ah, I think they are? Similar to how constructors can be reused, we could have a function fun assign(vec : vector<a>, idx : int, v : a) : vector<a> that returns a vector which is equal to vec except that the element at idx has been replaced by v. Then you can represent the code above without using any local variables.

We should, but due to the effect issue, we really need a way to qualify a polymorphic effect variable to be linear.

I don't think that you need to make this restriction. What do you think of this implementation:

import std/core/vector
import std/core/undiv
import std/core/unsafe

extern import {
  c file "test5.c"
}
// test5.c:
// static inline kk_box_t kk_identity(kk_box_t x, kk_context_t* ctx) {
//    return x; }

extern unsafe-cast(a : a) : b
  c "kk_identity"
  
fun unsafe-assign(v : vector<a>, i : int, x : a) : vector<a>
  unsafe-total fn() ->
    var v' := v
    v'[i] := x
    v'

fun unsafe-read(v : vector<a>, i : int) : a
  unsafe-total fn() -> v[i]

fun my/map(v : vector<a>, f : a -> e b) : e vector<b>
  fun go(vec, i)
    if i >= vector/length(vec)
      then vec
      else
        val v = unsafe-read(vec, i)
        val vec' = unsafe-assign(vec, i, unsafe-cast(f(v)))
        go(vec', pretend-decreasing(i + 1))
  unsafe-cast(go(v, 0))

effect choice
  ctl choice() : int

fun main()
  var a := vector-init-total(3, fn(i) 0)
  a[1] := 1
  val xs =
    with handler
      return(x) [x]
      ctl choice()
        resume(0) ++ resume(1)
    my/map(a,fn(x) abs(x - choice()))
  xs.map(fn(v) -> my/map(v, show).join(",").println())
  ()

This prints:

0,1,0
0,1,1
0,0,0
0,0,1
1,1,0
1,1,1
1,0,0
1,0,1

[TimWhiting]

For multiple resumptions it makes sense that it would end up copying, but always filling the vector completely.

However, I don't think that is safe for all effects. If the function f threw an exception and you were changing types you could end up with a mutated vector that is no longer vector<a>, but also not vector<b>.

Good point about the default value (your implementation example would need a default value to allow for fip values as well). However, the default value still suffers from the fact that an exception could cause you to lose the old value in the vector and not have a new value either. So it isn't just a temporary value, it is actually changing the semantics, even if you restrict the map function to return the same type.

Unfortunately although the runtime does set a flag if it is yielding for a final ctl operation, we don't know that until the rhs is actually yielding and after we have assigned a default value. Even then the operation clause could choose to only conditionally resume. It needs to be guaranteed in the type system to always resume (though I guess it could resume multiple times like you state).

[TimWhiting]

it isn't the vectors that are providing destructive update by themselves

Ah, I think they are? Similar to how constructors can be reused, we could have a function fun assign(vec : vector<a>, idx : int, v : a) : vector<a> that returns a vector which is equal to vec except that the element at idx has been replaced by v. Then you can represent the code above without using any local variables.

Sorry, I meant that currently they do not.

[TimWhiting]

It also looks like we have a different potential issue with the observability of destructive updates

Hmm, I agree that this behavior could be counter-intuitive, but for me the output is exactly what I would have expected. Conceptually, the finally runs after all computations so far, and it seems sensible to me that the local variables may have been mutated so far.

By this I meant that there is not an equivalent way to express this in pure Koka + effects.
As illustrated in this section of the Koka book: https://koka-lang.github.io/koka/doc/book.html#sec-combine
To get the non-transactional semantics of local state, the handler for state would have to be outside the exception effect handler, which would be a global transform, not a local transform. So in a sense it would almost make more sense to make local variables have transactional semantics. I'm not saying that the current behavior should change, but just illustrating how it could be confusing.

[anfelor]

However, I don't think that is safe for all effects. If the function threw an exception and you were changing types you could end up with a mutated vector that is no longer vector<a>, but also not vector<b>.

Yes, I agree that this is a terrible hack. But I think this is safe: If you throw an exception and throw the partially overwritten vector away, the runtime immediately calls drop on the vector, which does not care about types.

[TimWhiting]

True, I guess the only way it mutates is if it is unique, so it's not really a drop, it is a free.

[TimWhiting]

Given this discussion I think we need to do the following:

• Adjust the map function to use in-place updates when the vector is unique
• Provide another version of map that takes a default value to use for fip updates
• Add another api for local variable vectors (update(default, fn(old) -> old...)) that assigns the default value and allows for in place updates to the value in the vector.
• Consider other vector functions besides map, such as assignment which would return copies on non-unique reference counts.

If you need a vector to be mutable and a reference stored to it from a variety of datastructures (reference count would be > 1), that is precisely where a ref should be used.

Anything else, or is this all that is needed to address this issue @patrick-nicodemus?

As far as mutable variables and transactional / versus non-transactional semantics, that should probably go in a different issue. Maybe we could have another local variable definition form for that: immutable var.

[anfelor]

Provide another version of map that takes a default value to use for fip updates

We can already do this if we are happy to be less type-safe: Just define val null : int = 0 and write the else branch above as:

        val v = unsafe-read(vec, i)
        val vec' = unsafe-assign(vec, i, unsafe-cast(null))
        val vec'' = unsafe-assign(vec', i, unsafe-cast(f(v)))
        go(vec'', pretend-decreasing(i + 1))

[TimWhiting]

Daan actually already has a kk_box_null which he uses when initializing vectors (it's just in the runtime though, and not exposed as a koka value, so we would just need to do that via an extern, or provide a vec-clear(vec,index) extern).

[patrick-nicodemus]

Anything else, or is this all that is needed to address this issue @patrick-nicodemus?

@TimWhiting I think that sounds good to me but I'm not qualified to comment on precisely what should be implented here so if you change your mind later due to some reevaluation of the proper semantics then so be it. My main request is that whatever features are implemented are properly documented, as I said before the destructive update for vectors is not currently documented.

[patrick-nicodemus]

@anfelor Hi, sorry if this would be best left to a different issue, but you said

We currently use the same memory layout for all types of elements in the vector. This is in contrast to languages like C++, which specialize vectors to the type of the element. In practice, that can lead to much better cache usage. However, adding this to Koka would be a major change and we currently don't have the bandwidth to take on this project.

First, can you clarify whether this means that all vectors are vectors of "boxed" elements rather than "unboxed" values, and your comment to "cache usage" is referring to this additional dereferencing step?

Second, when you say "this would be a major change... we don't currently have the bandwidth" would it be a more feasible/realistic goal to do what OCaml does and introduce a dedicated array type of unboxed floats of a certain precision, the floatarray, or Bigarrays which would be specialized to the appropriate size, for a limited number of specific data types?

(Edit: apparently the distinction between floatarrays and Bigarrays in OCaml is that floatarrays live on the OCaml runtime heap and Bigarrays live in the C heap, floatarrays are more performant in OCaml code that rapidly allocates/deallocates them, according to this forum discussion -
not important here, but it is confusing that there are two different unboxed floating point array types)

[anfelor]

First, can you clarify whether this means that all vectors are vectors of "boxed" elements rather than "unboxed" values, and your comment to "cache usage" is referring to this additional dereferencing step?

Yes and yes. The only exception are integers, which are stored in the pointer if small enough.

would it be a more feasible/realistic goal to do what OCaml does and introduce a dedicated array type of unboxed floats of a certain precision,

Yes, you can do this quite easily already using the C FFI.