Top

Published in:

2017 | OriginalPaper | Chapter

Partiality and Container Monads

Authors : Tarmo Uustalu, Niccolò Veltri

Published in: Programming Languages and Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

previous chapter A Computational Interpretation of Context-Free Expressions

next chapter 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

Title: Partiality and Container Monads
Authors: Tarmo Uustalu
Niccolò Veltri
Publisher: Springer International Publishing
Book: Programming Languages and Systems
Print ISBN: 978-3-319-71236-9

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner