ABSTRACT
We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses.
We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.
- Roberto M. Amadio and Pierre-Louis Curien. Domains and Lambda-Calculi. Cambridge University Press, New York, NY, USA, 1998. Google ScholarDigital Library
- Brian Huffman. A purely definitional universal domain. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs '09), volume 5674 of LNCS, pages 260--275. Springer, 2009. Google ScholarDigital Library
- Brian Huffman. HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs. Ph.D. thesis, Portland State University, 2012.Google ScholarDigital Library
- Brian Huffman. Type constructor classes and monad transformers. Archive of Formal Proofs, June 2012. http://afp.sf.net/entries/Tycon.shtml, Formal proof development.Google Scholar
- Brian Huffman, John Matthews, and Peter White. Axiomatic constructor classes in Isabelle/HOLCF. In Joe Hurd and Tom Melham, editors, Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs '05), volume 3603 of LNCS, pages 147--162. Springer, 2005. Google ScholarDigital Library
- Mark P. Jones. Functional programming with overloading and higher-order polymorphism. In First International Spring School on Advanced Functional Programming Techniques, volume 925 of LNCS, Båstad, Sweden, May 1995. Springer-Verlag. Google ScholarDigital Library
- Olaf Müller, Tobias Nipkow, David von Oheimb, and Oskar Slotosch. HOLCF = HOLGoogle Scholar
- LCF. Journal of Functional Programming, 9:191--223, 1999. Google ScholarDigital Library
- Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL -- A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Oury. First-class type classes. In Otmane Ait Mohamed, César Munoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference (TPHOLs '08), volume 5170 of LNCS, pages 278--293. Springer, August 2008. Google ScholarDigital Library
- Philip Wadler. Theorems for free! In Functional Programming Languages and Computer Architecture, pages 347--359. ACM Press, 1989. Google ScholarDigital Library
Index Terms
- Formal verification of monad transformers
Recommendations
Formal verification of monad transformers
ICFP '12We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type ...
Monadic Type Systems
Pure type systems and computational monads are two parameterized frameworks that have proved to be quite useful in both theoretical and practical applications. We join the foundational concepts of both of these to obtain monadic type systems. ...
Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf
$\lambda$Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an ...
Comments