nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Partiality and Container Monads

verfasst von : Tarmo Uustalu, Niccolò Veltri

Erschienen in: Programming Languages and Systems

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

We investigate monads of partiality in Martin-Löf type theory, following Moggi’s general monad-based method for modelling effectful computations. These monads are often called lifting monads and appear in category theory with different but related definitions. In this paper, we unveil the relationship between containers and lifting monads. We show that the lifting monads usually employed in type theory can be specified in terms of containers. Moreover, we give a precise characterization of containers whose interpretations carry a lifting monad structure. We show that these conditions are tightly connected with Rosolini’s notion of dominance. We provide several examples, putting particular emphasis on Capretta’s delay monad and its quotiented variant, the non-termination monad.

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 A Computational Interpretation of Context-Free Expressions

Nächstes Kapitel The Negligible and Yet Subtle Cost of Pattern Matching

It is also called the partiality monad, but we want to use a more specific term here.

Notice that, if \(X:\mathcal {U}\), then \(\llbracket S,P \rrbracket ^\mathrm {c}\,X : \mathcal {U}_1\), i.e., \(\llbracket S,P \rrbracket ^\mathrm {c}\) would not be an endofunctor. But if \(X:\mathcal {U}_1\), then also \(\llbracket S,P \rrbracket ^\mathrm {c}\,X : \mathcal {U}_1\). Therefore we think of \(\llbracket S,P \rrbracket ^\mathrm {c}\) as a monad on \(\mathcal {U}_1\).

Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRefMATH

Ahman, D., Chapman, J., Uustalu, T.: When is a container a comonad? Log. Methods Comput. Sci. 10(3), article 14 (2014)

Altenkirch, T., Danielsson, N.A., Kraus, N.: Partiality, revisited. The partiality monad as a quotient inductive-inductive type. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 534–549. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_31 CrossRef

Altenkirch, T., Pinyo, G.: Monadic containers and universes (abstract). In: Kaposi, A. (ed.) Abstracts of 23rd International Conference on Types for Proofs and Programs, TYPES 2017, pp. 20–21. Eötvös Lórand University, Budapest (2017)

Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers–an overview. Math. Struct. Comput. Sci. 26(1), 38–88 (2016)MathSciNetCrossRefMATH

Bucalo, A., Führmann, C., Simpson, A.: An equational notion of lifting monad. Theor. Comput. Sci. 294(1–2), 31–60 (2003)MathSciNetCrossRefMATH

Capretta, V.: General recursion via coinductive types. Log. Methods Comput. Sci. 1(2), Article 1 (2005)

Chapman, J., Uustalu, T., Veltri, N.: Quotienting the delay monad by weak bisimilarity. Math. Struct. Comput. Sci. (to appear)

Cockett, J.R.B., Lack, S.: Restriction categories I: categories of partial maps. Theor. Comput. Sci. 270(1–2), 223–259 (2002)MathSciNetCrossRefMATH

10.

Cockett, J.R.B., Lack, S.: Restriction categories II: partial map classification. Theor. Comput. Sci 294(1–2), 61–102 (2003)MathSciNetCrossRefMATH

11.

Cockett, J.R.B., Lack, S.: Restriction categories III: colimits, partial limits, and extensivity. Math. Struct. Comput. Sci. 17(4), 775–817 (2007)MathSciNetCrossRefMATH

12.

Coquand, T., Mannaa, B., Ruch, F.: Stack semantics of type theory. In: Proceedings of 32th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 (2017)

13.

Escardó, M.H.: Synthetic topology of data types and classical spaces. Electron. Notes Theor. Comput. Sci. 87, 21–156 (2004)MATH

14.

Escardó, M.H., Knapp, C.M.: Partial elements and recursion via dominances in univalent type theory. In: Goranko, V., Dam, M. (eds.) Proceedings of 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, Leibniz International Proceedings in Informatics, vol. 82, article 21. Dagstuhl Publishing, Saarbrücken/Wadern (2017)

15.

Johnstone, P.T.: Topos Theory. London Mathematical Society Monographs, vol. 10. Cambridge University Press, Cambridge (1977)

16.

Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55–92 (1991)MathSciNetCrossRefMATH

17.

Norell, U.: Dependently typed programming in Agda. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 230–266. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04652-0_5 CrossRef

18.

Robinson, E., Rosolini, G.: Categories of partial maps. Inf. Comput. 79(2), 95–130 (1988)MathSciNetCrossRefMATH

19.

Rosolini, G.: Continuity and Effectiveness in Topoi. DPhil thesis, University of Oxford (1986)

20.

Univalent Foundations Program, The: Homotopy Type theory: Univalent Foundations of Mathematics. Institute for Advanced Study, Princeton, NJ (2013). http://homotopytypetheory.org/book

21.

Uustalu, T.: Container combinatorics: monads and lax monoidal functors. In: Mousavi, M.R., Sgall, J. (eds.) TTCS 2017. LNCS, vol. 10608, pp. 91–105. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-319-68953-1_8 CrossRef

22.

Uustalu, T., Veltri, N.: The delay monad and restriction categories. In: Hung, D.V., Kapur, D. (eds.) ICTAC 2017. LNCS, vol. 10580, pp. 32–50. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-319-67729-3_3

Titel: Partiality and Container Monads
verfasst von: Tarmo Uustalu
Niccolò Veltri
Verlag: Springer International Publishing
Buch: Programming Languages and Systems
Print ISBN: 978-3-319-71236-9

Electronic ISBN: 978-3-319-71237-6

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-71237-6_20

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