Comment by boltzmann-brain

2 days 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.

17 comments

boltzmann-brain

Reply
avsm  2 days ago

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  2 days 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.

AlotOfReading  2 days ago

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

  • whatis991  2 days ago

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

    • AlotOfReading  2 days ago

      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.

      2 replies →

aseipp  2 days ago

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  2 days ago

    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

3836293648  2 days ago

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