patternMinor
Can properties such as memory usage of a function be expressed in a dependently typed language?
Viewed 0 times
suchcanpropertiesexpresseddependentlyfunctionlanguageusagetypedmemory
Problem
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?
Solution
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.
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.
Context
StackExchange Computer Science Q#65716, answer score: 8
Revisions (0)
No revisions yet.