5 ms·
it's a massive crime that decades into FP, we still don't have a type system that can infer or constrain the amount of copies and allocations a piece of code ha
by boltzmann-brain 8mo ago
it's a massive crime that decades into FP, we still don't have a type system that can infer or constrain the amount of copies and allocations a piece of code has. software would be massively better if it did - unnecessary copies and space leaks are some of the most performance-regressing bugs out there and there simply isn't a natural way of unearthing those.
- AlotOfReading 8mo agoAllocations and copies are one of the things substructural typing formalizes. It's how E.g. Rust essentially eliminates implicit copies.
- whatis991 8mo agoI think I've heard of Rust devs complaining about moves having implicit bitwise copies that were not optimized away.
- AlotOfReading 8mo agoTraits with Copy can do that, I'm just saying they're not really implicit copies because it's a core, visible part of the language that the developer can control on all of their own types.
- whatis991 8mo agoBut do bitwise copies when moving not also possibly incur that, even without Copy? If the optimizer doesn't optimize it away? Since movement can happen by copying bits and releasing the old bits, as long as there is no UnsafeCell in the type, or something along those lines? https://www.reddit.com/r/rust/comments/vo31dw/comment/ieao7vu/ https://www.reddit.com/r/rust/comments/vo31dw/comment/ieao7v...
- zozbot234 8mo agoAvoiding bitwise moves requires either costly indirection or else some sort of express place semantics where some program values are meant to be accessed in a fixed pattern such as stack-like access (most common) or perhaps other kinds, such as deque, sequence, tree etc. Substructural types can help model this but doing so correctly is not always easy.
- avsm 8mo agoWe do now though, with OxCaml! The local stack allocation mode puts in quite a strong constraint on the shape of the allocations that are possible. On my TODO list next is to hook up the various O(x)Caml memory profiling tools: we have statmemprof which does statistical sampling, and then the runtime events buffer, and (hopefully) stack activity in OxCaml's case from the compiler. This provides a pretty good automation loop for a performance optimising coding agent: it can choose between heap vs local, or copy vs reference, or fixed layout (for SIMD) vs fragmentation (for multicore NUMA) depending on the tasks at hand. Some references: - Statmemprof in OCaml : https://tarides.com/blog/2025-03-06-feature-parity-series-statmemprof-returns/ https://tarides.com/blog/2025-03-06-feature-parity-series-st... - "The saga of multicore OCaml" by Ron Minsky about how Jane Street viewed performance optimisation from the launch of OCaml 5.0 to where they are today with OxCaml https://www.youtube.com/watch?v=XGGSPpk1IB0 https://www.youtube.com/watch?v=XGGSPpk1IB0
- zozbot234 8mo ago> infer or constrain the amount of copies and allocations a piece of code has That's exactly what substructural logic/type systems allows you to do. Affine and linear types are one example of substructural type systems, but you can also go further in limiting moves, exchanges/swaps etc. which helps model scenarios where allocation and deallocation must be made explicit.
- NeutralForest 8mo agoI don't think it's been integrated in any mainstream language though.
- DonaldPShimoda 8mo agoI think by default Rust uses affine types, but that's about the extent of it.
- NeutralForest 8mo agoI know some research languages are playing around with linear types, I wonder if we'll see it show up in some language or another.
- johnbender 8mo agohttps://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line... Experimental and of course one can debate whether Haskell is mainstream but I figured it merits a mention.
- boltzmann-brain 8mo agodo they allow the following? https://news.ycombinator.com/item?id=46859860 https://news.ycombinator.com/item?id=46859860
- aseipp 8mo agoThere are ongoing projects like Granule[1] that are exploring more precise resource usage to be captured in types, in this case by way of graded modalities. There is of course still a tension in exposing too much of the implementation details via intensional types. But it's definitely an ongoing avenue of research. [1] http://granule-project.github.io/granule.html http://granule-project.github.io/granule.html
- boltzmann-brain 8mo agocan Granule let me specify the following constraints on a function? - it will use O(n) space where n is some measure of one of the parameters (instead of n you could have some sort of function of multiple measures of multiple parameters) - same but time use instead of space use - same but number of copies - the size of an output will be the size of an input, or less than it - the allocated memory after the function runs is less than allocated memory before the function runs - given the body of a function, and given that all the functions used in the body have well defined complexities, the complexity of the function being defined with them is known or at least has a good upper bound that is provably true
- 3836293648 8mo agoThere is discussion about this in the Rust world, though no attempts at implementation (and yet further from stabilisation)
- zokier 8mo agoWouldn't such analysis in the general case run afoul of Rices theorem?
- cryptonector 8mo agohttps://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line...