Reason for filter's result being alias-free, but partition's result not?

[johannes-riecken]

I find Futhark's type system fascinating, and while playing around, I noticed that filter's result is alias-free, but that of partition is aliasing:

filter : [n] 'a (a -> bool) ([n]a): *[]a
partition : [n] 'a (a -> bool) ([n]a): ?[k].([k]a, [n-k]a)

I didn't quite understand why that is, given that in-place partitioning is a bit like in-place filtering without the final length truncation?
Totally fine if that was an arbitrary decision. I just find it important that I understand the types of the most basic functions in detail.

[athas]

I don't think we thought carefully about it, but the reason is that partition ends by taking two slices of the same array and then returning them - that means they are aliased (as far as Futhark is concerned), although we of course know that they will not truly be aliased.

This can be changed in two ways:

1. Take a copy at the end of filter, although the caller might as well do that.
2. Make a built-in magical split that understands that the two arrays cannot alias.