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

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