When we define
data List a = Nil | Cons a (List a)
in Haskell, we know that we have defined the type of finite or infinite lists. This is because Haskell has recursive types. As a result, the possibility of [divergence] is deeply built into the system.
Instead, we would prefer to be able to have a type of the form
data Stream a = Cons a (Stream a)
The values of Stream a are meant to be productive, infinite streams of a's. Moreover, we would like to be able to compute with types such as Stream a without introducing nontermination - in the style of total functional programming.
To achieve that, one replaces general recursion by guarded recursion.
The first calculus to be explicitly called guarded by its creator is a Martin-Löf type theory with principles for guarded recursive definitions for non-well-founded trees given by [Coquand 1994].
A coinductive definition on an infinite object can only be admitted if it is productive. That is: every now and then, it will produce visible output. Telling whether a coinductive definition is productive is difficult. It is traditionally achieved by ad-hoc syntactic checks on the definition of a function. Both Coq and Agda feature such productivity checking mechanisms.
However, productivity checking can often fail. It is often too conservative on higher-order functions, rejecting definitions that might be productive if given the right higher-order arguments (but maybe not otherwise). Thus, it is natural to seek a more compositional approach to checking whether a function is productive.
[Nakano 2000] suggested the use of types. More specifically, the idea is to introduce a modality on types. The idea is that, for every type , the type classifies expressions which will produce a value of type after a computation step (or: after a tick of the clock, in the next step, etc.).
For example, a term
is a function which, given an later, will produce an now. If we have such a function, we can feed it to a guarded fixed point combinator
which will productively produce an .
Moreover, if we are in a type-theoretic setting with universes, we can use guarded fixed points on the universe to define all sorts of interesting types. For example, we can define the type of streams as the fixed point
Every term of type consists of a value of type now, as well as the rest of the stream. However, we can only access the rest of the stream later.
This approach was semantically considered by [Birkedal et al. 2011], and syntactically formulated in a HoTT context by [Birkedal and Møgelberg 2013].
However, type theories based on the later modality are not very expressive. One of the main reasons for the lack of expressivity is that every object defined in them must be not just productive, but also causal.
Causality has a very particular meaning. Every type can be thought of as existing over time - or maybe indexed in a global clock. For example, we cannot write a program that decides whether to sell or buy a stock today based on its price tomorrow. This function is productive, as it will return a decision if given tomorrow's prices. However, it is not causal: we cannot look into the future to make this decision today.
A more prosaic, programming-oriented example is the 'every other' function, which returns every other element of a stream:
every2nd :: Stream a -> Stream a
every2nd (Cons x (Cons y ys)) = Cons x (every2nd ys)
This does not type-check if Stream a is defined to be an a now and a Stream a later, as ys is available under two 'laters' - and so in two time steps from now. It is, however, a productive definition.
Causality is a very good guarantee for some forms of programming which are strongly 'on the clock,' like functional reactive programming. However, when we just wish for coinductive definitions to be productive, causality is too strong. The problem is thus to relax causality into productively
[Atkey and McBride 2013] proposed a solution to this problem by introducing the notion of clocks. A clock is an "abstract time stream" along which objects are defined. Instead of a single modality , we have a modality for every clock . A term of type classifies a value that will be available after one tick of clock . One can have multiple clocks at once, indexing multiple "logical" time streams.
The key construction over clocks is clock quantification. For each type involving clock , one can quantify over it to obtain a type . An expression of that type (with no other free clocks) is one whose value can be obtained at any time, including right now.
Atkey and McBride formulate a simple type system with clocks and guarded recursion. They also show how to extend this to inductive types. They also define a realizability semantics, where clocks correspond to step-indexing, and clock quantification to taking a big intersection over sets of realizers as they vary over the step index.
The idea of clocks has found applications in augmenting Martin-Löf type theory with guarded recursion.
In particualr, the following type theories have been proposed:
The following type theory does not use clocks, but provides for guarded recursion:
Coquand, Thierry. 1994. ‘Infinite Objects in Type Theory’. In Types for Proofs and Programs, edited by Henk Barendregt and Tobias Nipkow, 806:62–78. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-58085-9_72.
@inproceedings{coquand_1994,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Infinite objects in type theory},
volume = {806},
doi = {10.1007/3-540-58085-9_72},
booktitle = {Types for {Proofs} and {Programs}},
publisher = {Springer Berlin Heidelberg},
author = {Coquand, Thierry},
editor = {Barendregt, Henk and Nipkow, Tobias},
year = {1994},
pages = {62--78}
}
Nakano, H. 2000. ‘A Modality for Recursion’. In Fifteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2000), 255–66. IEEE Computer Society. https://doi.org/10.1109/LICS.2000.855774.
@inproceedings{nakano_2000,
title = {A modality for recursion},
doi = {10.1109/LICS.2000.855774},
booktitle = {Fifteenth {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS} 2000)},
publisher = {IEEE Computer Society},
author = {Nakano, H.},
year = {2000},
pages = {255--266}
}
Birkedal, Lars, Rasmus Møgelberg, Jan Schwinghammer, and Kristian Støvring. 2012. ‘First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees’. Logical Methods in Computer Science 8 (4). https://doi.org/10.2168/LMCS-8(4:1)2012.
@article{birkedal_2012,
title = {First steps in synthetic guarded domain theory: step-indexing in the topos of trees},
volume = {8},
doi = {10.2168/LMCS-8(4:1)2012},
number = {4},
journal = {Logical Methods in Computer Science},
author = {Birkedal, Lars and M{\o}gelberg, Rasmus and Schwinghammer, Jan and St{\o}vring, Kristian},
year = {2012}
}
Birkedal, Lars, and Rasmus Ejlers Møgelberg. 2013. ‘Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes’. In 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 213–22. IEEE. https://doi.org/10.1109/LICS.2013.27.
@inproceedings{birkedal_2013,
title = {Intensional {Type} {Theory} with {Guarded} {Recursive} {Types} qua {Fixed} {Points} on {Universes}},
doi = {10.1109/LICS.2013.27},
booktitle = {2013 28th {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE},
author = {Birkedal, Lars and Møgelberg, Rasmus Ejlers},
year = {2013},
pages = {213--222}
}
Atkey, Robert, and Conor McBride. 2013. ‘Productive Coprogramming with Guarded Recursion’. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, 197–208. New York, NY, USA: Association for Computing Machinery. https://doi.org/10.1145/2500365.2500597.
@inproceedings{atkey_2013,
address = {New York, NY, USA},
title = {Productive {Coprogramming} with {Guarded} {Recursion}},
doi = {10.1145/2500365.2500597},
booktitle = {Proceedings of the 18th {ACM} {SIGPLAN} {International} {Conference} on {Functional} {Programming}},
publisher = {Association for Computing Machinery},
author = {Atkey, Robert and McBride, Conor},
year = {2013}
pages = {197--208}
}
Møgelberg, Rasmus Ejlers. 2014. ‘A Type Theory for Productive Coprogramming via Guarded Recursion’. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). ACM. https://doi.org/10.1145/2603088.2603132.
@inproceedings{moegelberg_2014,
title = {A type theory for productive coprogramming via guarded recursion},
doi = {10.1145/2603088.2603132},
booktitle = {Proceedings of the {Joint} {Meeting} of the {Twenty}-{Third} {EACSL} {Annual} {Conference} on {Computer} {Science} {Logic} ({CSL}) and the {Twenty}-{Ninth} {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
publisher = {ACM},
author = {M{\o}gelberg, Rasmus Ejlers},
year = {2014}
}
Bizjak, Aleš, and Rasmus Ejlers Møgelberg. 2015. ‘A Model of Guarded Recursion With Clock Synchronisation’. Electronic Notes in Theoretical Computer Science 319: 83–101. https://doi.org/10.1016/j.entcs.2015.12.007.
@article{bizjak_2015,
title = {A {Model} of {Guarded} {Recursion} {With} {Clock} {Synchronisation}},
volume = {319},
doi = {10.1016/j.entcs.2015.12.007},
journal = {Electronic Notes in Theoretical Computer Science},
author = {Bizjak, Ale\v{s} and M{\o}gelberg, Rasmus Ejlers},
year = {2015},
pages = {83--101}
}
Bizjak, Aleš, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal. 2016. ‘Guarded Dependent Type Theory with Coinductive Types’. In Foundations of Software Science and Computation Structures, edited by Bart Jacobs and Christof Löding, 9634:20–35. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49630-5_2.
@inproceedings{bizjak_2016,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Guarded {Dependent} {Type} {Theory} with {Coinductive} {Types}},
volume = {9634},
doi = {10.1007/978-3-662-49630-5_2},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer Berlin Heidelberg},
author = {Bizjak, Ale\v{s} and Grathwohl, Hans Bugge and Clouston, Ranald and M{\o}gelberg, Rasmus E. and Birkedal, Lars},
editor = {Jacobs, Bart and Löding, Christof},
year = {2016},
pages = {20--35}
}
Bahr, Patrick, Hans Bugge Grathwohl, and Rasmus Ejlers Møgelberg. 2017. ‘The Clocks Are Ticking: No More Delays!’ In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE. https://doi.org/10.1109/LICS.2017.8005097.
@inproceedings{bahr_clocks_2017,
title = {The clocks are ticking: {No} more delays!},
url = {http://www.itu.dk/people/mogel/papers/lics2017.pdf},
doi = {10.1109/LICS.2017.8005097},
booktitle = {2017 32nd {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} ({LICS})},
publisher = {IEEE},
author = {Bahr, Patrick and Grathwohl, Hans Bugge and M{\o}gelberg, Rasmus Ejlers},
year = {2017}
}
Jonathan Sterling and Robert Harper. 2018. Guarded Computational Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18). https://doi.org/10.1145/3209108.3209153
@inproceedings{sterling_2018,
author = {Sterling, Jonathan and Harper, Robert},
title = {Guarded Computational Type Theory},
year = {2018},
publisher = {Association for Computing Machinery},
doi = {10.1145/3209108.3209153},
booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science}
}
Palombi, Daniele, and Jonathan Sterling. 2023. "Classifying topoi in synthetic guarded domain theory." In Electronic Notes in Theoretical Informatics and Computer Science 1. https://doi.org/10.46298/entics.10323
@article{palombi_2023,
title={Classifying topoi in synthetic guarded domain theory},
author={Palombi, Daniele and Sterling, Jonathan},
journal={Electronic Notes in Theoretical Informatics and Computer Science},
doi= {10.46298/entics.10323},
year={2023},
publisher={Episciences. org}
}
Birkedal, Lars, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. 2019. ‘Guarded Cubical Type Theory’. Journal of Automated Reasoning 63 (2): 211–53. https://doi.org/10.1007/s10817-018-9471-7.
@article{birkedal_2019,
title = {Guarded {Cubical} {Type} {Theory}},
volume = {63},
doi = {10.1007/s10817-018-9471-7},
number = {2},
journal = {Journal of Automated Reasoning},
author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
year = {2019},
pages = {211--253}
}
Møgelberg, Rasmus Ejlers, and Niccolò Veltri. 2019. ‘Bisimulation as Path Type for Guarded Recursive Types’. Proceedings of the ACM on Programming Languages 3 (POPL): 1–29. https://doi.org/10.1145/3290317.
@article{mogelberg_2019,
title = {Bisimulation as path type for guarded recursive types},
volume = {3},
doi = {10.1145/3290317},
number = {POPL},
journal = {Proceedings of the ACM on Programming Languages},
author = {M{\o}gelberg, Rasmus Ejlers and Veltri, Niccol\`{o}},
year = {2019},
pages = {1--29}
}