Using type-level programming to tag functions with time and space complexity

I was wondering if anyone had done work on tagging functions at the type level with their time or space complexity and, if it's even feasible, calculating the complexity of compound functions. Any pointers? Cheers Daniel

Hello, Oleg, Chung-chieh Shan, and others have done some work close to this area. On this page, see the "Monads parameterized by time" section: http://okmij.org/ftp/Haskell/number-parameterized-types.html Also see this page: http://okmij.org/ftp/Haskell/types.html#ls-resources The new type family stuff being introduced in to GHC should hopefully go a long way towards making this type of code more readable. Not sure how easy or hard it would be to enforce the particular properties you mentioned, but the above references might give you some idea how to proceed. j. At Fri, 19 Oct 2007 09:00:49 +1300, Daniel McAllansmith wrote:
I was wondering if anyone had done work on tagging functions at the type level with their time or space complexity and, if it's even feasible, calculating the complexity of compound functions.
Any pointers?
Cheers Daniel _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

On Thu, 18 Oct 2007, Daniel McAllansmith
I was wondering if anyone had done work on tagging functions at the type level with their time or space complexity and, if it's even feasible, calculating the complexity of compound functions.
Any pointers?
I have done some work on this in the context of dependently typed languages. See "Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures" (http://www.cs.chalmers.se/~nad/publications/danielsson-popl2008.html). The paper also lists some related work which may be useful to you. -- /NAD
participants (3)
-
Daniel McAllansmith
-
Jeremy Shaw
-
Nils Anders Danielsson