Some linear type systems garantee that functions defined in them have polynomial time complexity: http://www.cs.cmu.edu/~fp/courses/15816-s12/misc/hofmann03ic... http://www.kurims.kyoto-u.ac.jp/~terui/lalcjournal.pdf It appears however that the ones developed so far are awkward to "program" in.