Resource Analysis with Refinement Types
Please log in to watch this conference skillscast.
Liquid Haskell is an extension of Haskell’s Type system that allows annotating types with refinement predicates. It’s great for ensuring the correctness of your code, but it can also be used to improve the performance of your code.
If you track your resources then Liquid Haskell can be used to statically bound the resources needed at runtime, thus statically deciding how performant your code is. You are liquidating your assets.
To track resource we define a `Tick monad that ticks each time a resource (ranging recursive calls to thunks) is used. Then we use refinement types to statically approximate the number of ticks that can occur at runtime. This reasoning aids runtime code optimization, since it can be used to compare resource usage of two different programs.
In this talk, I will present this technique through small examples (sorting algorithms and mapping) and discuss the advantage and current limitations on real-world code adaptation.
Q&A
Question: Could be useful for proving bounds on open file descriptors in FFI code? (if you put the Ticks in the right places). Niki, the talk covered well the idea of generating ticks, but since some resources (FDs, memory, etc) can be released, how easy is it to model that concept with LH?
Answer: That sounds like a very good application!
Release is just a negative cost, so it is easy to model! There is no requirement
for the cost to be non-negative; so just need to define release x = Tick
-1 x.
BTW, the actual implementation give you a cost n x = Tick n x
operator.
Question: Refinement types and the sort of theorem proving you're doing here seem to have some overlap with the dependent haskell efforts. Both attempt to prove more and more sophisticated properties using types. How do you see these efforts working together in the future?
Answer: It would be great for liquid types and dependent Haskell to work together. Though, it seems to be quite difficult, because they underlying used logics are quite different (SMT, classic logic for liquid types and Coq-style constructive logic for dependent Haskell).
So, there is not an active plan to merge the two reasonings, but indeed it would be amazing if we did!
Resources:
You can play with Liquid Haskell using our online demo: http://goto.ucsd.edu:8090/index.html#?demo=SimpleRefinements.hs
But, recently we turned it into a ghc-plugin, so you can use it by just adding the ghc-options: -fplugin=LiquidHaskell option on your cabal file (e.g., https://github.com/kosmikus/popl21-liquid-haskell-tutorial/blob/master/popl21-liquid-haskell-tutorial.cabal#L9).
The standard applications are checking termination and totality of your functions (these checks are performed by default) and list indexing properties. You can also use it in this “theorem-proving style” mode that I presented to prove any fancy program “meta-properties”.
YOU MAY ALSO LIKE:
Thank you to our sponsors and partners
Platinum
Silver
Bronze
Resource Analysis with Refinement Types
Niki Vazou
Research Assistant Professor
IMDEA Software Institute