LiquidHaskell Refinement Types for Haskell

on YouTube ↗01h 43m

" summary

Covers refinement types and LiquidHaskell: extending Haskell’s type system with logical predicates to specify and verify value-dependent properties. Describes what LiquidHaskell can check—examples include totality (e.g., whether head can crash), termination (e.g., whether mergeSort loops), memory-safety (SEGFAULTs), and correctness invariants for libraries such as containers, hscolour, bytestring, text, vector-algorithms and xmonad.

AI-written summary · about

" chapters (9)

1. 0:00Start
2. 15:04Exercise: Positive Integers
3. 16:13Predicate Subtyping
4. 17:26Example: Natural Numbers
5. 30:12Specifying the Length of a List
6. 32:00Exercise: Partial Functions
7. 39:14Exercise: map
8. 56:04Exercise: Ordered Pairs
9. 58:20Exercise: Valid CSV Tables

" related talks

• 01h 57mTypes as Program Specifications: A Intro to Type-Level Programming in HaskellThomas Dietert · LambdaConf 2019
• 01h 03mHow to use Phantom Types and Existential Types in ProductionHarold Carr · LambdaConf 2020 Global Edition
• 35mThe Mastermind behind Refinement TypesJorge Mayoral, Juanjo Madrigal · Lambda World 2025
• 45mDepending on TypesStephanie Weirich · Code Mesh 2015
• 55mKeynote: Propositions as TypesPhilip Wadler · Code Mesh 2015
• 39mDependent Types in HaskellStephanie Weirich · Strange Loop 2017
• 01h 12mTruth about TypesBartosz Milewski · Lambda Days 2016
• 56mWrite You Some Proofs for Great GoodRobert Peszek · LambdaConf 2019