nach oben

Journal of Automated Reasoning

Erschienen in:

10.07.2018

Effect Polymorphism in Higher-Order Logic (Proof Pearl)

verfasst von: Andreas Lochbihler

Erschienen in: Journal of Automated Reasoning | Ausgabe 2/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Vorheriger Artikel Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory

Nächster Artikel A Verified Generational Garbage Collector for CakeML

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

Available in the Archive of Formal Proofs at https://www.isa-afp.org/entries/Monomorphic_Monad.html.

Type variables that appear in the signature of locale parameters are fixed for the whole locale. In particular, the value type

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figaw_HTML.gif

cannot be instantiated inside the locale

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figax_HTML.gif

or its extension

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figay_HTML.gif

. The interpreter

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figaz_HTML.gif

, however, returns

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figba_HTML.gif

s. For this reason,

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figbb_HTML.gif

is defined in an extension of

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figbc_HTML.gif

that merely specialises

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figbd_HTML.gif

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figbe_HTML.gif

. For readability, I usually omit this detail in this article.

Continuation parameters like

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figdc_HTML.gif

’s and

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figdd_HTML.gif

’s make it possible to circumvent the restriction to monomorphic values. More generally, if we made every definition take a continuation, like in continuation-passing style, we would regain value polymorphism. In doing so, we would however lose that sequencing of computations and control flow is captured by a small number of (primitive) operations. Instead, every definition could implement arbitrary control flow, like in a continuation monad. Thus, we would need a lot more lemmas to reason about sequencing. In a commutative monad, e.g., one commutativity lemma would be needed for every pair of definitions. In contrast, my approach needs just one assumption comm to express commutativity of sequencing (Sect. 2.5), and a few assumptions about the primitive operations, e.g., sample-comm (Sect. 2.3).

In my monad implementations in Sect. 3, sampling is relationally parametric for arbitrary relations

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figeu_HTML.gif

, so I could drop the restriction

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figev_HTML.gif

. However, this would unnecessarily exclude some other implementations as all my abstract proofs so far used only

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figew_HTML.gif

relations.

The support of

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figfz_HTML.gif

is the set of elementary events with positive probability:

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figga_HTML.gif

iff

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figgb_HTML.gif

The conference paper [23] demanded sample-cong instead of sample-param. Parametricity is a better condition as it allows us to rename choices like in the biased coin flip example above.

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

Isabelle’s

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figti_HTML.gif

feature, which resolves overloading during type checking, cannot be used either as it does not support recursive resolutions. For example, resolving

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figtj_HTML.gif

takes two steps: first to

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figtk_HTML.gif

and then to

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figtl_HTML.gif

. 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.

Following the “as abstract as possible” spirit of this paper, I actually proved the identities in the locale of commutative monads and showed that

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figyd_HTML.gif

is commutative if its inner monad is.

The alternative applicative interface [16] with the operator

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figys_HTML.gif

is amenable to monomorphisation if we restrict ourselves to infinite value types

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figyt_HTML.gif

as then

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figyu_HTML.gif

is isomorphic to

https://static-content.springer.com/image/art%3A10.1007%2Fs10817-018-9476-2/MediaObjects/10817_2018_9476_Figyv_HTML.gif

. This interface is tailored towards a first-order language [10]. So functions must be uncurried and their arguments encoded using the isomorphism. We would thus clutter the definitions and proofs with conversions and lose the benefits of built-in higher-order unification.

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

Back, R.J., Wright, J.: Refinement Calculus—A Systematic Introduction. Springer, Berlin (1998)CrossRefMATH

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 MathSciNetCrossRefMATH

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)

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

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

Erwig, M., Kollmansberger, S.: Functional pearls: probabilistic functional programming in Haskell. J Funct Program 16, 21–34 (2006). https://doi.org/10.1017/S0956796805005721 CrossRefMATH

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

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

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

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

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

13.

Huffman, B.: Formal verification of monad transformers. In: ICFP 2012, pp. 15–16. ACM (2012). https://doi.org/10.1145/2364527.2364532

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

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

16.

Hutton, G.: Higher-order functions for parsing. J. Funct. Program. 2(3), 323–343 (1992)MathSciNetCrossRefMATH

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

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

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

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

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 CrossRefMATH

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)

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

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

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

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

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)

Titel: Effect Polymorphism in Higher-Order Logic (Proof Pearl)
verfasst von: Andreas Lochbihler
Publikationsdatum: 10.07.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 2/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9476-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2/2019

Canonicity for Cubical Type Theory

Preface: Special Issue on Homotopy Type Theory and Univalent Foundations

A Formalization of Convex Polyhedra Based on the Simplex Method

From Signatures to Monads in UniMath

The Univalence Axiom in Cubical Sets

Categoricity Results and Large Model Constructions for Second-Order ZF in Dependent Type Theory