Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad
summary
Defines a small DSL that models laziness with explicit delay/force, counts steps with a tick and runs property tests via QuickCheck to check persistent amortized costs. Uses defunctionalized thunks so counterexamples are printable. Tests all lazy structures in Okasaki's book and rediscovers a previously unreported gap in persistent Finger Trees; three cases fail the lightweight check (bankers queue needs a credit inheritance proof, catenable lists and the implicit catenable deck remain unresolved). Package and examples live on Hackage.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 1:05Why amortized time complexity matters
- 4:17Persistent queues and lazy evaluation
- 6:45Credit Monad for Haskell
- 9:12Modeling Okasaki’s implicit queue
- 13:32Credit passing style
- 14:37Testing with QuickCheck
- 17:29Defunctionalizing laziness
- 19:57Debugging with Credit Monad
- 20:41Limitations and future work
- 21:48Q&A: Credit Monad package
- 23:11Q&A: Applicability to queues
- 24:55Q&A: Bugs found
- 25:39Q&A: Production translation
- 26:22Q&A: Binary operations testing
- 27:08Q&A: Garbage collection
related talks
20mType-level Property Based Testing
02h 38mLazy Evaluation
46mTesting in the world of Functional Programming
36mWorking Hard to Keep Things Lazy
49mA Practical Introduction to Eff in Haskell
24mCatching space leaks at compile-time using th-deepstrict
41mWhy the free Monad isn't free
31mBoring use cases for exciting types