Top

Published in:

2017 | OriginalPaper | Chapter

The Delay Monad and Restriction Categories

Authors : Tarmo Uustalu, Niccolò Veltri

Published in: Theoretical Aspects of Computing – ICTAC 2017

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

We continue the study of Capretta’s delay monad as a means of introducing non-termination from iteration into Martin-Löf type theory. In particular, we explain in what sense this monad provides a canonical solution. We discuss a class of monads that we call \(\omega \)-complete pointed classifying monads. These are monads whose Kleisli category is an \(\omega \)-complete pointed restriction category where pure maps are total. All such monads support non-termination from iteration: this is because restriction categories are a general framework for partiality; the presence of an \(\omega \)-join operation on homsets equips a restriction category with a uniform iteration operator. We show that the delay monad, when quotiented by weak bisimilarity, is the initial \(\omega \)-complete pointed classifying monad in our type-theoretic setting. This universal property singles it out from among other examples of such monads.

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 Institutions for Behavioural Dynamic Logic with Binders

next chapter Logical Characterisation of Parameterised Bisimulations

\(\mathsf {C}\) is typed \(\mathcal {U}_1 \rightarrow \mathcal {U}_1\), so it is an endofunctor on \(\mathbf {Set}_1\). But as the other examples can be replayed for any \(\mathcal {U}_k\), comparing this example to them is unproblematic.

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). doi:10.1007/978-3-662-54458-7_31 CrossRef

Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 115–130. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_10 CrossRef

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., Guo, X.: Join restriction categories and the importance of being adhesive. Abstract of talk presented at CT 2007 (2007)

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

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

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

10.

Danielsson, N.A.: Operational semantics using the partiality monad. In: Proceedings of 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 127–138. ACM, New York (2012)

11.

Ésik, Z., Goncharov, S.: Some remarks on Conway and iteration theories. arXiv preprint arXiv:1603.00838 (2016)

12.

Goncharov, S., Rauch, C., Schröder, L.: Unguarded recursion on coinductive resumptions. Electron. Notes Theor. Comput. Sci. 319, 183–198 (2015)MathSciNetCrossRefMATH

13.

Guo, X.: Products, joins, meets, and ranges in restriction categories. Ph.D. thesis, University of Calgary (2012)

14.

Hofmann, M.: Extensional Constructs in Intensional Type Theory. CPHS/BCS Distinguished Dissertations. Springer, London (1997). doi:10.1007/978-1-4471-0963-1 CrossRef

15.

Mulry, P.S.: Partial map classifiers and partial cartesian closed categories. Theor. Comput. Sci. 136(1), 109–123 (1994)MathSciNetCrossRefMATH

16.

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). doi:10.1007/978-3-642-04652-0_5 CrossRef

17.

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

18.

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

Title: The Delay Monad and Restriction Categories
Authors: Tarmo Uustalu
Niccolò Veltri
Publisher: Springer International Publishing
Book: Theoretical Aspects of Computing – ICTAC 2017
Print ISBN: 978-3-319-67728-6

Electronic ISBN: 978-3-319-67729-3

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-67729-3_3

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