You've found a Premium Feature!
Certain videos, events and workspaces require a Premium Membership. Become a Skills Matter Premium Member today to access exclusive benefits including free tickets to online conferences, Members-only events and discounts on training.Unlock this Video
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.
YOU MAY ALSO LIKE:
- Liquid Haskell: Theorem Proving for All (SkillsCast recorded in December 2018)
- Haskell eXchange 2021 (Online Conference on 16th - 17th November 2021)
- Abstract Fun-sense: a functional perspective on life (SkillsCast recorded in May 2021)
- Eliminating Bugs with Dependently Typed Haskell (SkillsCast recorded in May 2021)