Liquid Haskell Tutorial

BOB 2018, Berlin, 2018-02-23

Andres Löh

Acknowledgements

Thanks to the entire Liquid Haskell team for producing such a fantastic tool, including the interactive web environment used for this tutorial.

Special thanks to Ranjit Jhala and Niki Vazou for tirelessly answering all my questions during the preparation of this tutorial.

Contents

• 1. Introduction
• 1.1. What is Liquid Haskell?
• 1.2. More precise types
• 1.3. An extension of Haskell
• 1.4. Refinement types
• 1.5. Type synonyms
• 1.6. Refinement types must refine
• 1.7. One expression, many types
• 1.8. Refinement types and functions
• 1.9. Preconditions vs. postconditions
• 1.10. Integer arithmetic
• 1.11. Exercises
• 2. Lists
• 2.1. Goal
• 2.2. Our own list type
• 2.3. Termination
• 2.4. Measures
• 2.5. Mapping
• 2.6. Interleaving two lists
• 2.7. Disabling termination checking
• 2.8. Totality
• 2.9. Impossible cases
• 2.10. Exercises
• 2.11. Taking elements out of a list
• 2.12. Dropping elements from a list
• 2.13. Computing s sublist
• 2.14. Replicating an element
• 2.15. Computing a range of numbers
• 2.16. Safe indexing
• 2.17. Bonus exercises
• 2.18. Finding equal elements
• 2.19. Grouping elements
• 2.20. Run-length encoding
• 3. Sets
• 3.1. Uninterpreted functions
• 3.2. Using an uninterpreted function
• 3.3. Sets
• 3.4. Lookup tables
• 3.5. Another measure on maps
• 3.6. A safe lookup function
• 3.7. Removing bindings
• 4. Proofs
• 4.1. Tables again
• 4.2. Reflecting functions
• 4.3. Proving a simple property
• 4.4. And a slightly more complicated one ...
• 4.5. A property on lists
• 5. Conclusions