Do (static) type systems exist which attempt to formalize the performance characteristics of programs? I cannot find seem to find such attempts.

Since type systems are (one of) the most powerful tools in the programmer's arsenal to make statements about programs, and since there are many instances in which performance is critical, it would not seem to be far-fetched to imagine attempts had been undertaken to create a type system which attempts to make at least some statements about the storage and runtime characteristics of programs.

  • 1
    What would your type system say about the performance of if condition then expensive_operation else cheap_operation? – svick Jul 6 '15 at 14:19
  • I know there were developments in using abstract interpretation to automatically infer worst-case complexity of code (and termination). You may be interested in it... – Bakuriu Jul 6 '15 at 14:42
  • Not wholly related, but still: kernelnewbies.org/FAQ/LikelyUnlikely In the Linux kernel/gcc compiler are likely / unlikely macros to optimize certain paths. E.g. if (likely(operation_went_fine)) { // Do something } else if (unlikely(error_occured)) { // Do something else } – AmazingDreams Jul 6 '15 at 14:53
  • The volatile and register keywords in C come to mind. – mattnz Jul 7 '15 at 0:58

You could imagine a type system sophisticated enough to be related to WCET or complexity of the program. Then, the issue is to make a sound type analyzer (or checker) - i.e. typing rules - to make that possible, and implement it efficiently enough to make that reasonably useful.

Most of the type systems are simple enough to be quick to compute in practice (at least for the reasonable set of programs a human developer could manually write).

Some academic programming languages (e.g. AGDA) have very sophisticated type systems which are Turing-complete, so their compiler may take a large (perhaps infinite) amount of time.

(If I understand well, Jérémie Salvucci's PhD work in progress at LIP6 in Paris is quite related to your question; I have sent him an email about it; you might look for regions and types...).

Be however aware of Rice's theorem & the Halting problem. Type systems might not always be the silver bullet you might want them to be (see the old no silver bullet book).

  • 4
    WCET is "Worst case execution time" in this context (in case anyone other than me wonders) – Klaas van Schelven Jul 6 '15 at 10:58
  • 9
    Dependently-typed languages like Agda, Coq, Epigram, Guru, Isabelle, etc. "solve" the Halting Problem, Rice's Theorem and friends by not being Turing-complete. Either by construction (i.e. it is simply not possible to write an infinite loop / non-terminating recursion), by requiring that all programs must be written in such a way that the termination checker can prove termination, or by requiring the programmer to submit a machine-checkable termination proof. – Jörg W Mittag Jul 6 '15 at 12:11

It seems eminently possible to create a type system which categorises the performance characteristic of types (e.g. "fast/slow for serial access, "fast/slow for random access", "memory efficient/inefficient"). Those traits could be abstract types placed into the hierarchy in such a way that the more concrete types inherited from them. However, the performance of any program using those types would depend upon the way they are actually used/accessed. For the type system to make statements about the program itself, usage of (access to) those types would have itself to be represented as types. This would mean forgoing the use of built-in control structures (e.g. for/while loops) and instead using types which implement them. Hence the hierarchy could have an abstract serial-access type and descendant list-serial-access, tree-serial-access types and so on. Efficiency of usage might then be at least partly expressed by the combination and application of these types to each other.

In a functional language like Haskell - which has almost no control structures anyway - this looks to me fairly practical and enforceable. In Java, however, such a system seems much less achievable (not so much from the implementation as from the enforceability/trustworthiness of the result).

Haskell already allows us to state definitively how much of a program is pure and provides ways of confining particular activities within sealed boxes. Since parallelism/concurrency in Haskell is implemented through the type system, it could be argued that it is already part of the way there (to what you want). In contrast, imperative languages (even statically typed ones like Java) offer the coder many, many ways to subvert any attempt at this.

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.