×

Effect polymorphism in higher-order logic (proof pearl). (English) Zbl 1468.68062

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

MSC:

68N18 Functional programming and lambda calculus
68N20 Theory of compilers and interpreters
68Q60 Specification and verification (program logics, model checking, etc.)
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Back, R.J., Wright, J.: Refinement Calculus—A Systematic Introduction. Springer, Berlin (1998) · Zbl 0949.68094 · doi:10.1007/978-1-4612-1674-2
[2] Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123-153 (2014). https://doi.org/10.1007/s10817-013-9284-7 · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7
[3] Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: ITP 2014. LNCS, vol. 8558, pp. 93-110. Springer (2014) · Zbl 1416.68151
[4] Bulwahn, L., Krauss, A., Haftmann, F., Erkök, L., Matthews, J.: Imperative functional programming with Isabelle/HOL. In: TPHOLs 2008. LNCS, vol. 5170, pp. 134-149. Springer (2008). https://doi.org/10.1007/978-3-540-71067-7_14 · Zbl 1165.68352
[5] 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 (2015). https://doi.org/10.1007/978-3-662-46669-8_4 · Zbl 1335.68037
[6] Erwig, M., Kollmansberger, S.: Functional pearls: probabilistic functional programming in Haskell. J Funct Program 16, 21-34 (2006). https://doi.org/10.1017/S0956796805005721 · Zbl 1091.68023 · doi:10.1017/S0956796805005721
[7] Gibbons, J., Hinze, R.: Just do it: simple monadic equational reasoning. In: ICFP 2011, pp. 2-14. ACM (2011). https://doi.org/10.1145/2034773.2034777 · Zbl 1323.68207
[8] Grimm, N., Maillard, K., Fournet, C., Hriţcu, C., Maffei, M., Protzenko, J., Ramananandro, T., Rastogi, A., Swamy, N., Zanella Béguelin, S.: A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. In: CPP 2018, pp. 130-145. ACM (2018). https://doi.org/10.1145/3167090
[9] Harrison, W.L.: The essence of multitasking. In: Johnson, M., Vene, V. (eds.) Algebraic Methodology and Software Technology (AMAST 2006). LNCS, vol. 4019, pp. 158-172. Springer (2006). https://doi.org/10.1007/11784180_14 · Zbl 1236.68038
[10] Hinze, R.: Lifting operators and laws. http://www.cs.ox.ac.uk/ralf.hinze/Lifting.pdf. Accessed 12 June 2018 (2010)
[11] Hölzl, J., Lochbihler, A., Traytel, D.: A formalized hierarchy of probabilistic system types. In: ITP 2015. LNCS, vol. 9236, pp. 203-220. Springer (2015). https://doi.org/10.1007/978-3-319-22102-1_13 · Zbl 1465.68199
[12] 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 (2009). https://doi.org/10.1007/978-3-642-03359-9_18 · Zbl 1252.68257
[13] Huffman, B.: Formal verification of monad transformers. In: ICFP 2012, pp. 15-16. ACM (2012). https://doi.org/10.1145/2364527.2364532 · Zbl 1291.68145
[14] Huffman, B., Kunčar, O.: Lifting and Transfer: a modular design for quotients in Isabelle/HOL. In: CPP 2013. LNCS, vol. 8307, pp. 131-146. Springer (2013). https://doi.org/10.1007/978-3-319-03545-1_9 · Zbl 1426.68284
[15] Huffman, B., Matthews, J., White, P.: Axiomatic constructor classes in Isabelle/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs. LNCS, vol. 3603, pp. 147-162. Springer (2005). https://doi.org/10.1007/11541868_10 · Zbl 1152.68521
[16] Hutton, G.: Higher-order functions for parsing. J. Funct. Program. 2(3), 323-343 (1992) · Zbl 0817.68097 · doi:10.1017/S0956796800000411
[17] Jeuring, J., Jansson, P., Amaral, C.: Testing type class laws. In: Haskell 2012, pp. 49-60. ACM (2012). https://doi.org/10.1145/2364506.2364514
[18] Kunčar, O.: Correctness of Isabelle’s cyclicity checker: implementability of overloading in proof assistants. In: CPP 2015, pp. 85-94. ACM (2015). https://doi.org/10.1145/2676724.2693175
[19] Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft’s algorithm. In: ITP 2012. LNCS, vol. 7406, pp. 166-182. Springer (2012). https://doi.org/10.1007/978-3-642-32347-8_12 · Zbl 1360.68757
[20] Liang, S., Hudak, P., Jones, M.: Monad transformers and modular interpreters. In: POPL 1995, pp. 333-343. ACM (1995). https://doi.org/10.1145/199448.199528
[21] Lobo Vesga, E.: Hacia la formalización del razonamiento ecuacional sobre mónadas. Technical report, Universidad EAFIT (2013). http://hdl.handle.net/10784/4554
[22] Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP. LNCS, vol. 9632, pp. 503-531. Springer (2016). https://doi.org/10.1007/978-3-662-49498-1_20 · Zbl 1335.68033
[23] Lochbihler, A.: Effect polymorphism in higher-order logic (proof pearl). In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving (ITP 2017), vol. 10499, pp. 389-409. Springer (2017). https://doi.org/10.1007/978-3-319-66107-0_25 · Zbl 1468.68061
[24] 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 (2016). https://doi.org/10.1007/978-3-319-43144-4_16 · Zbl 1464.68063
[25] Mitchell, J.C.: Representation independence and data abstraction. In: POPL 1986, pp. 263-276. ACM (1986). https://doi.org/10.1145/512644.512669
[26] Moggi, E.: An abstract view of programming languages. Technical report ECS-LFCS-90-113, LFCS, School of Informatics, University of Edinburgh (1990)
[27] Nipkow, T., Klein, G.: Concrete semantics. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-10542-0 · Zbl 1410.68004 · doi:10.1007/978-3-319-10542-0
[28] 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 (2005) · Zbl 1152.68529
[29] Piróg, M., Gibbons, J.: The coinductive resumption monad. In: Mathematical Foundations of Programming Semantics (MFPS 2014). ENTCS, vol. 308, pp. 273-288 (2014). https://doi.org/10.1016/j.entcs.2014.10.015 · Zbl 1337.68189
[30] Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL 2002, pp. 154-165. ACM (2002). https://doi.org/10.1145/503272.503288 · Zbl 1323.68150
[31] Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP 1983. Information Processing, vol. 83, pp. 513-523. North-Holland/IFIP (1983)
[32] Sternagel, C., Thiemann, R.: A framework for developing stand-alone certifiers. In: Ayala-Rincón, M., Mackie, I. (eds.) Logical and Semantic Frameworks with Applications (LSFA 2014), vol. 312, pp. 51-67. ENTCS (2015). https://doi.org/10.1016/j.entcs.2015.04.004 · Zbl 1342.68304
[33] Wadler, P.: How to replace failure by a list of successes: a method for exception handling, backtracking, and pattern matching in lazy functional languages. In: Jouannaud, J.P. (ed.) Functional Programming Languages and Computer Architecture (FPCA 1985). LNCS, vol. 201, pp. 113-128. Springer (1985). https://doi.org/10.1007/3-540-15975-4_33 · Zbl 0568.68007
[34] Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) Advanced Functional Programming. LNCS, vol. 925, pp. 24-52. Springer (1995). https://doi.org/10.1007/3-540-59451-5_2
[35] 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 (1997). https://doi.org/10.1007/BFb0028402
[36] Wimmer, S., Hu, S., Nipkow, T.: Verified memoization and dynamic programming. In: Avigad, J., Mahboubi, A. (eds.) Interactive theorem proving. ITP 2018. LNCS, vol. 10895, pp. 579-596. Springer, Cham (2018) · Zbl 1511.68094
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.