[boltzmann-brain]

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.

[avsm]

We 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-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

[zozbot234]

> 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]

I don't think it's been integrated in any mainstream language though.

[johnbender]

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.

[DonaldPShimoda]

I think by default Rust uses affine types, but that's about the extent of it.

[NeutralForest]

I know some research languages are playing around with linear types, I wonder if we'll see it show up in some language or another.

[boltzmann-brain]

do they allow the following? https://news.ycombinator.com/item?id=46859860

[AlotOfReading]

Allocations and copies are one of the things substructural typing formalizes. It's how E.g. Rust essentially eliminates implicit copies.

[whatis991]

I think I've heard of Rust devs complaining about moves having implicit bitwise copies that were not optimized away.

[AlotOfReading]

Traits 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]

But 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/ieao7v...

[zozbot234]

Avoiding 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.

[aseipp]

There 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

[boltzmann-brain]

can 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

[cryptonector]

https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/line...

[3836293648]

There is discussion about this in the Rust world, though no attempts at implementation (and yet further from stabilisation)

[zokier]

Wouldn't such analysis in the general case run afoul of Rices theorem?