11
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ In this video Brian McKenna provides an example of encoding time complexity into types. $\endgroup$ – Anton Trunov Nov 8 '16 at 6:33
8
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.