Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2017: Interactive Theorem Proving pp 389–409Cite as

Effect Polymorphism in Higher-Order Logic (Proof Pearl)

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10499))

Abstract

The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. We show that if a monad is used with values of only one type, this notion can be formalised in HOL. Based on this idea, we develop a library of effect specifications and implementations of monads and monad transformers. Hence, we can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. We illustrate the usefulness of effect polymorphism with a monadic interpreter.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Type variables that appear in the signature of locale parameters are fixed for the whole locale. In particular, the value type cannot be instantiated inside the locale or its extension . The interpreter , however, returns s. For this reason, is defined in an extension of that merely specialises . For readability, we usually omit this detail in this paper.

  2. 2.

    Such environments can be nicely handled by applying a reader monad transformer on top (Sect. 4).

  3. 3.

    Isabelle’s feature, which resolves overloading during type checking, cannot be used either as it does not support recursive resolutions. For example, resolving takes two steps: first to and then to . The second step fails due to the intricate interleaving of type checking and resolution. Even if this is just an implementation issue, resolving overloading during type checking prevents definitions that are generic in the monad, which general overloading supports.

  4. 4.

    Following the “as abstract as possible” spirit of this paper, we actually proved the identities in the locale of commutative monads and showed that is commutative if its inner monad is.

  5. 5.

    http://www.infsec.ethz.ch/research/projects/FCSPI.html.

References

  1. Ballarin, C.: Locales: a module system for mathematical theories. J. Automat. Reason. 52(2), 123–153 (2014)

    Article  MathSciNet  Google Scholar 

  2. Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: Klein, G., Gamboa, R. (eds.) ITP 2014. LNCS, vol. 8558, pp. 93–110. Springer, Cham (2014). doi:10.1007/978-3-319-08970-6_7

    Chapter  Google Scholar 

  3. Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: Ait Mohamed, O., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134–149. Springer, Heidelberg (2008). doi:10.1007/978-3-540-71067-7_14

    Chapter  Google Scholar 

  4. Eberl, M., Hölzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80–104. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46669-8_4

    Chapter  Google Scholar 

  5. Erwig, M., Kollmansberger, S.: Functional pearls: probabilistic functional programming in Haskell. J. Funct. Program. 16, 21–34 (2006)

    Article  Google Scholar 

  6. Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: ICFP 2011, pp. 2–14. ACM (2011)

    Google Scholar 

  7. Hölzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 203–220. Springer, Cham (2015). doi:10.1007/978-3-319-22102-1_13

    Chapter  Google Scholar 

  8. Homeier, P.V.: The HOL-Omega logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 244–259. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_18

    Chapter  Google Scholar 

  9. Huffman, B.: Formal verification of monad transformers. In: ICFP 2012, pp. 15–16. ACM (2012)

    Google Scholar 

  10. Huffman, B., Kunčar, O.: Lifting and Transfer: a modular design for quotients in Isabelle/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131–146. Springer, Cham (2013). doi:10.1007/978-3-319-03545-1_9

    Chapter  MATH  Google Scholar 

  11. Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 147–162. Springer, Heidelberg (2005). doi:10.1007/11541868_10

    Chapter  MATH  Google Scholar 

  12. Jeuring, J., Jansson, P., Amaral, C.: Testing type class laws. In: Haskell 2012, pp. 49–60. ACM (2012)

    Google Scholar 

  13. Kunčar, O.: Correctness of Isabelle’s cyclicity checker: implementability of overloading in proof assistants. In: CPP 2015, pp. 85–94. ACM (2015)

    Google Scholar 

  14. Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166–182. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32347-8_12

    Chapter  Google Scholar 

  15. Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: POPL 1995, pp. 333–343. ACM (1995)

    Google Scholar 

  16. Lobo Vesga, E.: Hacia la formalización del razonamiento ecuacional sobre mónadas. Technical report, Universidad EAFIT (2013). http://hdl.handle.net/10784/4554

  17. Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503–531. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49498-1_20

    Chapter  MATH  Google Scholar 

  18. Lochbihler, A.: Effect polymorphism in higher-order logic. Archive of Formal Proofs (2017). Formal proof development. http://isa-afp.org/entries/Monomorphic_Monad.shtml

  19. Lochbihler, A., Schneider, J.: Equational reasoning with applicative functors. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 252–273. Springer, Cham (2016). doi:10.1007/978-3-319-43144-4_16

  20. Mitchell, J.C.: Representation independence and data abstraction. In: POPL 1986, pp. 263–276. ACM (1986)

    Google Scholar 

  21. Moggi, E.: An abstract view of programming languages. Technical report ECS-LFCS-90-113, LFCS, School of Informatics, University of Edinburgh (1990)

    Google Scholar 

  22. Nipkow, T., Klein, G.: Concrete Semantics. Springer, Cham (2014). doi:10.1007/978-3-319-10542-0

    Book  MATH  Google Scholar 

  23. Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 385–396. Springer, Heidelberg (2005). doi:10.1007/11541868_25

    Chapter  Google Scholar 

  24. Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL 2002, pp. 154–165. ACM (2002)

    Google Scholar 

  25. Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995). doi:10.1007/3-540-59451-5_2

    Chapter  Google Scholar 

  26. Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997). doi:10.1007/BFb0028402

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank Dmitriy Traytel and the anonymous reviewers for suggesting many improvements to the presentation. This work is supported by the Swiss National Science Foundation grant 153217 “Formalising Computational Soundness for Protocol Implementations”.

Author information

Authors and Affiliations

  1. Institute of Information Security, Department of Computer Science, ETH Zurich, Zurich, Switzerland

    Andreas Lochbihler

Authors
  1. Andreas Lochbihler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andreas Lochbihler .

Editor information

Editors and Affiliations

  1. University of Brasília, Brasília D.F., Brazil

    Mauricio Ayala-Rincón

  2. NASA, Hampton, VA, USA

    César A. Muñoz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Lochbihler, A. (2017). Effect Polymorphism in Higher-Order Logic (Proof Pearl). In: Ayala-Rincón, M., Muñoz, C.A. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science(), vol 10499. Springer, Cham. https://doi.org/10.1007/978-3-319-66107-0_25

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66107-0_25

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66106-3

  • Online ISBN: 978-3-319-66107-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation