Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
summary
Extension to Liquid Haskell adds refined typeclasses in Liquid Haskell so class laws become checkable at Core; the implementation verifies laws for 34 instances across Semigroup, Monoid, Functor, Applicative and Monad, and uses Template Haskell to derive VRDT instances. A generic VRDT model is formalized and a strong convergence proof is machine-checked; concrete VRDTs include MultiSet, CausalTree and TwoPhaseMap. Two working apps (an event planner and a collaborative text editor) plus a Reflex-integrated client and operation-propagating server are implemented and the patch is being merged upstream.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:19Motivation
- 0:42Contributions
- 1:21Liquid Haskell
- 3:46Core Representation
- 5:13Refined Typeclasses
- 7:25Typeclass Laws
- 8:44Verified Replicated Data Types
- 10:00Strong convergence
- 10:29Primitive VRDTS
- 10:47Compound VRDTs
- 11:57VRDT Proofs
- 12:18Example Applications
- 14:52Summary
related talks
58mLiquidHaskell: Liquid Types for Haskell
31mTotal Type Classes
28mQuotient Polymorphism
57mApplied category theory and abstract algebra
59mHaskell Design Patterns for Genericity & Asynchronous Behavior
01h 04mLinear Haskell, Today and Tomorrow
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
31mDependently-Typed Programming with Logical Equality Reflection