nach oben

Erschienen in:

2017 | Supplement | Buchkapitel

Effect Polymorphism in Higher-Order Logic (Proof Pearl)

verfasst von : Andreas Lochbihler

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

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

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

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

Vorheriges Kapitel Typing Total Recursive Functions in Coq

Nächstes Kapitel Schulze Voting as Evidence Carrying Computation

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/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq37_HTML.gif

cannot be instantiated inside the locale

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq38_HTML.gif

or its extension

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq39_HTML.gif

. The interpreter

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq40_HTML.gif

, however, returns

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq41_HTML.gif

s. For this reason,

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq42_HTML.gif

is defined in an extension of

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq43_HTML.gif

that merely specialises

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq44_HTML.gif

. For readability, we usually omit this detail in this paper.

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

Isabelle’s

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq328_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/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq329_HTML.gif

takes two steps: first to

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq330_HTML.gif

and then to

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq331_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, we actually proved the identities in the locale of commutative monads and showed that

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-66107-0_25/978-3-319-66107-0_25_IEq460_HTML.gif

is commutative if its inner monad is.

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

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

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_7CrossRef

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_14CrossRef

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_4CrossRef

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

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

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_13CrossRef

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_18CrossRef

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

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_9CrossRefMATH

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_10CrossRefMATH

12.

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

13.

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

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_12CrossRef

15.

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

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_20CrossRefMATH

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)

21.

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

22.

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

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_25CrossRef

24.

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

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_2CrossRef

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/BFb0028402CrossRef

Titel: Effect Polymorphism in Higher-Order Logic (Proof Pearl)
verfasst von: Andreas Lochbihler
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-66106-3

Electronic ISBN: 978-3-319-66107-0

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-66107-0_25

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 "Technik"

Springer Professional "Wirtschaft"

Premium Partner