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

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

[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?