4 ms·
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. The
by aseipp 8mo 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 http://granule-project.github.io/granule.html
- boltzmann-brain 8mo agocan 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