Invalid uniqueness simplification on trivial program

[athas]

Somewhat surprisingly, the compiler messes this up:

let main (xs: *[]i32) =
  let xs' = zip xs xs
  let xs'[0] = (0,0)
  in xs'

[athas]

I'm not even sure this should be type correct.

[athas]

The program should work, but we need to stop pretending the intrinsic zip doesn't need to copy its input - it does. (Although in many cases this copy can be simplified away later.) I just need to figure out whether the problem is rooted in this intrinsic, or whether it can be provoked without using any dubiously typed intrinsics.

[athas]

The root of the problem is this: our implementation strategy for zip has been to turn it into a no-op, because we always keep arrays of pairs "unzipped" in the core IR. This is generally fine, but it is not with respect to uniqueness, because consuming the result of zip xs xs does not just "consume xs once", it consumes it twice (if there is an aliasing relationship). Hence this aliasing relationship should not exist, and when I'm done fixing this, it won't. We have decent copy-elimination optimisations in the simplifier, so hopefully this will not have negative performance impact (but if it does, tough luck, correctness is more important).

[melsman]

Wouldn't an alternative be to have two kinds of zip: one that takes two unique arrays and returns a unique array and one that returns a non-unique array? man. 15. mar. 2021 kl. 22.52 skrev Troels Henriksen < ***@***.***>:

…

The program should work, but we need to stop pretending the intrinsic zip doesn't need to copy its input - it does. (Although in many cases this copy can be simplified away later.) I just need to figure out whether the problem is rooted in this intrinsic, or whether it can be provoked without using any dubiously typed intrinsics. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#1271 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAI5DOYMONRLK3X3DNOTYATTDZ6TFANCNFSM4ZHJ737Q> .

[melsman]

I guess that besides from zip and zipU, we would also need a zipC that returns a unique array by copying... tir. 16. mar. 2021 kl. 14.17 skrev Martin Elsman ***@***.***>:

…

Wouldn't an alternative be to have two kinds of zip: one that takes two unique arrays and returns a unique array and one that returns a non-unique array? man. 15. mar. 2021 kl. 22.52 skrev Troels Henriksen < ***@***.***>: > The program should work, but we need to stop pretending the intrinsic zip > doesn't need to copy its input - it does. (Although in many cases this copy > can be simplified away later.) I just need to figure out whether the > problem is rooted in this intrinsic, or whether it can be provoked without > using any dubiously typed intrinsics. > > — > You are receiving this because you are subscribed to this thread. > Reply to this email directly, view it on GitHub > <#1271 (comment)>, > or unsubscribe > <https://github.com/notifications/unsubscribe-auth/AAI5DOYMONRLK3X3DNOTYATTDZ6TFANCNFSM4ZHJ737Q> > . >

[athas]

No, because uniqueness in Futhark isn't really uniqueness. If you have a function f : a -> a, then even though the value produced by f x is not unique, you can still consume it, if you can consume x (because there is an aliasing relationship). This was added precisely so we didn't need unique/nonunique variants of functions like transpose and zip. The alternative would be a significant complication of the type system to add "uniqueness polymorphism". In programming languages with linear types, this often takes the form of "multiplicity polymorphism", which can get quite complicated (see Linear Haskell).

In Futhark, uniqueness only matters across function calls (so in function types essentially), and plays two roles:

• Inside a function, you can consume parameters that are marked as unique.
• A unique return value of a function will not alias any of the function arguments.

(There's a few more rules; e.g. inside a function you cannot consume anything that is free in the function.)