Push arrays/fold

[Divesh-Otwani]

Summary

This PR adds to push arrays:

• folds and unzip and closes Push Arrays #80
• more flexible construction and closes Construction of Push Arrays #62

Depends on #287.

Things I don't fully understand

• I don't fully understand the role of linear types here. Is it just to have the linear monoid so that the type necessarily writes each element once (and that in the allocation, we use destination arrays). Can we come up with a concise statement of how we apply linear types?
• Aren't we still missing the "use each index only once" property of pull arrays?

[b-mehta]

This and part 1 looks promising to me! I think foldWith looks sensible, and if unzip can be made to work then I'd be much more convinced. Nice stuff!

[utdemir]

Suggested change

	unzip = undefined
	unzip (Array k) = k (\(a, b) -> (singleton a, singleton b))

This kind of make sense to me, but I'm unsure (both semantically and performance-wise).

[Divesh-Otwani]

That's very clever and I feel dumb for not coming up with it after messing with it for a while, lol 😸

It does make sense: k is something that takes something that writes an a to a monoid that represents a composable way to write an a to a cell of an array. Here, k takes something that changes (a,b) to a monoidal-computation that writes an (a,b) to a cell of an array.

This implementation in words says "a way to write each pair of (a,b) into a monoidal writing-computation is to have a pair of monoidal writing-computations". If you give this to k it will make a bunch of pairs of singletons and concatenate them.

[utdemir]

This function is foldMap (specialized to Array and with a linear arrow), so I think we should call it that.

The Foldable/Traversable issues are likely relevant, but those assume the first parameter to be linear too. Bit unfortunate that we don't have a typeclass for this.

[utdemir]

I don't think we need this.

[Divesh-Otwani]

Remnants from my testing.

[utdemir]

This also doesn't seem to be necessary.

[Divesh-Otwani]

Remnants from my testing.

[dpulls]

🎉 All dependencies have been resolved !