Modular Effects in Haskell Through Effect Polymorphism and Explicit Dictionary Applications: A New Approach and the μVeriFast Verifier As a Case Study

Research output: Chapter in Book/Report/Conference proceedingConference paper

1 Citation (Scopus)
196 Downloads (Pure)

Abstract

In applications with a complex structure of side-effects, effects should be dealt with modularly: components should be programmed against abstract effect interfaces that other components can instantiate as required, and reusable effect patterns should be factored out from the rest of the application. In this paper, we study a new, general approach to achieve this in Haskell by combining effect polymorphism and the recently proposed coherent explicit dictionary applications. We demonstrate the elegance and generality of our approach in μVeriFast: a Haskell-based reimplementation of the semi-automatic separation-logic-based verification tool VeriFast. This implementation features a complex interplay of advanced side-effects: a backtracking search of program paths with angelic and demonic non-determinism, interaction with an underlying off-the-shelf SMT solver, and mutable state that is either backtracked or not during the search. Our use of effect polymorphism improves over the current non-modular implementation of VeriFast, allows us to nicely factor out the backtracking search pattern as a new AssumeAssert monad, and enables advanced features involving effects, such as the non-intrusive addition of a graphical symbolic debugger based on delimited continuations.
Original languageEnglish
Title of host publicationProceedings of the 12th ACM SIGPLAN International Symposium on Haskell
Place of PublicationNew York, NY, USA
PublisherACM
Pages1-14
Number of pages14
ISBN (Electronic)9781450368131
ISBN (Print)978-1-4503-6813-1
DOIs
Publication statusPublished - 8 Aug 2019
Event12th ACM SIGPLAN International Haskell Symposium - Berlin, Germany
Duration: 22 Aug 201923 Aug 2019
Conference number: 12
https://www.haskell.org/haskell-symposium/2019/

Publication series

NameHaskell 2019 - Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, co-located with ICFP 2019

Conference

Conference12th ACM SIGPLAN International Haskell Symposium
Abbreviated titleHaskell ’19
CountryGermany
CityBerlin
Period22/08/1923/08/19
Internet address

Keywords

  • Haskell
  • backtracking search
  • effect polymorphism
  • modular effects
  • monads
  • separation logic
  • symbolic execution

Fingerprint

Dive into the research topics of 'Modular Effects in Haskell Through Effect Polymorphism and Explicit Dictionary Applications: A New Approach and the μVeriFast Verifier As a Case Study'. Together they form a unique fingerprint.

Cite this