zlacker

>>noelwe+(OP)
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.

>>boltzm+wy
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

>>aseipp+0Y
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