Practical Verification of the Reader Monad
A. Haršáni (TU Delft - Electrical Engineering, Mathematics and Computer Science)
J.G.H. Cockx – Mentor (TU Delft - Programming Languages)
L.F.B. Escot – Mentor (TU Delft - Programming Languages)
Qing Wang – Graduation committee member
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Agda2hs is a tool that allows developers to write verified programs using Agda and then translate these programs to Haskell while maintaining the verified properties. Previous research has shown that Agda2hs can be used to produce a verified implementation of a wide range of programs. However, monads that model effectful computations were largely unexplored in the context of Agda2hs. In this paper, we investigate the Reader monad, which gives us a way to model the global state. As monads are in practice commonly combined with other monads, we also investigate the transformer ReaderT. This paper provides the implementation of Reader and ReaderT in Agda, verifies its properties based on laws of type classes functor, applicative, and monad, as well as monad transformer laws for ReaderT, and assesses whether Agda2hs produces their correct and useful translation.