alt Hacker NewsThere 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.
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