Suppose one wants to reason about properties of code beyond things like totality and functional purity - one also cares about the memory consumption, or algorithmic complexity of a function. Can this be done through dependent typing and effects systems?
$\begingroup$
$\endgroup$
1
-
2$\begingroup$ In this video Brian McKenna provides an example of encoding time complexity into types. $\endgroup$– Anton TrunovCommented Nov 8, 2016 at 6:33
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
Yes, it can. While conceptually it's not that difficult, it hasn't been studied all that much. One aspect of the field is cost semantics such as the research done by Guy Blelloch.
In the vein of the video Anton mentioned is Daniellson's work in Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures. This does indeed use a monad to carry around a cost per operation. A similar monad, at the semantic level, is used in Denotational cost semantics for functional languages with inductive types. Here's a 2016 paper doing something similar in Coq, A Coq Library For Internal Verification of Running-Times.
The NuPRL people have also long been interested in doing things like this. In Expressing Computational Complexity in Contstructive Type Theory, which basically amounts to calculating over a structured operational semantics. Where it gets a bit more interesting is that you can reflect the language semantics into the language. The example in the final section, section 12, of Naive Computational Type Theory illustrates and discusses this sort of thing.
answered Nov 8, 2016 at 7:51