Verifying replicated data types with typeclass refinements in Liquid Haskell
Abstract
This paper presents an extension to Liquid Haskell that facilitates stating and semi-automatically proving properties of typeclasses. Liquid Haskell augments Haskell with refinement types —our work allows such types to be attached to typeclass method declarations, and ensures that instance implementations respect these types. The engineering of this extension is a modular interaction between GHC, the Glasgow Haskell Compiler, and Liquid Haskell’s core proof infrastructure. The design sheds light on the interplay between modular proofs and typeclass resolution, which in Haskell is coherent by default (meaning that resolution always selects the same implementation for a particular instantiating type), but in other dependently typed languages is not.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 13, 2020
- Source ID
- 10.1145/3428284
Entities
People
- J. E. S. Parker
- Lindsey Kuper
- Michael Hicks
- Niki Vazou
- Patrick L Redmond
- Yiyun Liu
Organizations
- Amazon
- Defense Advanced Research Projects Agency
- Instituto Madrileño de Estudios Avanzados
- National Science Foundation
- University of California, Santa Cruz
- University of Maryland