<p>The main purpose of clocks in guarded type theories (originating in <a href="https://dl.acm.org/doi/10.1145/2500365.2500597" rel="nofollow noreferrer">Atkey &amp; McBride ICFP 2013</a>) is so that we can define <em>coinductive</em> constructions from guarded recursive definitions.</p>
<p>Semantically this coinductive construction seems most naturally modeled by the <em>global sections</em> modality <span class="math-container">$\square$</span> on the topos of trees which takes a step indexed set <span class="math-container">$(X_i)_{i &lt; \omega}$</span> to the constant presheaf of &quot;<span class="math-container">$\omega$</span>-chains&quot;, i.e., a family of elements <span class="math-container">$x_i \in X_i$</span> that commutes with the restriction functions.</p>
<p>However I have seen very few papers on guarded recursion use this modality, instead they axiomatize a type of clocks <span class="math-container">$K$</span> and use the clock quantification type <span class="math-container">$\forall k. X$</span> for essentially the same purpose. The corresponding models are somewhat more complicated (essentially presheaves over a family of natural numbers rather than just one), and the manipulation of clocks is at least somewhat tedious, so I wonder what the advantage of multiple clocks is over using a &quot;single-clock&quot; model like the topos of trees and the <span class="math-container">$\square$</span> modality? The only paper I have seen advocate for the <span class="math-container">$\square$</span> modality is <a href="https://dl.acm.org/doi/10.1145/3514241" rel="nofollow noreferrer">Gratzer, Cavallo, Kavvos, Guatto &amp; Birkedal, TOCL 2022</a> but there it is just a small example.</p>

CC BY-SA 4.0
2022-08-09T01:23:55.397Z
I am not exactly well-versed in models of guarded type theories, but the discussion at https://www.cs.cmu.edu/~rwh/papers/guarded/lics.pdf Guarded computational type theory, sections causality and then "Programming applications" just before section 1.1 motivates why the clocks were introduced. I am not sure, (it might be interesting to check) if the TOCL 2022 paper admits the "drop every second element" program without adding clocks.
Ilk
CC BY-SA 4.0
2022-08-09T11:12:00.953Z
Your example should work fine with $\square$ in that $\square \triangleright A \cong \square A$ holds which is the key property that clock quantification has that makes it work.
Max New
CC BY-SA 4.0
2022-08-11T17:15:50.183Z
So actually a few of our papers have advocated for $\Box$ and $\rhd$ as the desirable primitives (the MTT papers actually use this as a motivating example, and the journal version at LMCS gives a rather long series of examples in this framework). My recollection is that $\Box$ was suggested in Clouston et al 2015 (Programming and Reasoning with Guarded Recursion for Coinductive Types). The main advantage of $\Box$ is conceptual simplicity: the same intended model, just one additional modality. The disadvantages are twofold: $\Box$ is much harder to handle proof-theoretically than clocks ....
daniel gratzer
CC BY-SA 4.0
2022-08-11T17:18:53.443Z
... and when one handles _nested_ guarded/coinductive types things become difficult: in order to even form $\Box \mathsf{Stream}(A)$ one needs to ensure that $A$ is constant, etc. In practice, I think it's mostly the former that wins out. To my knowledge, MTT was the first type theory which could handle both $\Box$ and $\rhd$ together, and that came out in 2020. On the other hand, clocked type theory and clocks in general are significantly easier to get off the ground syntactically... with the cost of far more complex semantics.
daniel gratzer
CC BY-SA 4.0
2022-08-11T19:23:35.740Z
"the former that wins out" the former meaning what here? Clocks?
Max New
CC BY-SA 4.0
2022-08-12T07:57:49.793Z
Ah sorry, I actually meant that one of the driving advantages of clocks has been that they were more easily shown to be syntactically feasible. Even though there are advantages with having multiple clocks etc, I think that the most important factor has just been that $\Box$ and $\rhd$ together was a bit thorny.
daniel gratzer
CC BY-SA 4.0
2022-08-12T13:53:32.737Z
Ok I think that's a good answer: Historically it's because clock-based systems were easier to define based on our understanding of modal type theory. And objectively it's less clear but nesting of recursive types is trickier.
Max New
<type-theory><dependent-type><ct.category-theory><step-indexing><guarded-domain-theory>
Why Multiple Clocks in Guarded Dependent Type Theories?
Max New
# Why Multiple Clocks in Guarded Dependent Type Theories?

(Asked by: username_0 on 2022-08-08)

The main purpose of clocks in guarded type theories (originating in [Atkey & McBride ICFP 2013](https://dl.acm.org/doi/10.1145/2500365.2500597)) is so that we can define *coinductive* constructions from guarded recursive definitions.

Semantically this coinductive construction seems most naturally modeled by the *global sections* modality $\square$ on the topos of trees which takes a step indexed set $(X\_i)\_{i < \omega}$ to the constant presheaf of "$\omega$-chains", i.e., a family of elements $x\_i \in X\_i$ that commutes with the restriction functions.

However I have seen very few papers on guarded recursion use this modality, instead they axiomatize a type of clocks $K$ and use the clock quantification type $\forall k. X$ for essentially the same purpose. The corresponding models are somewhat more complicated (essentially presheaves over a family of natural numbers rather than just one), and the manipulation of clocks is at least somewhat tedious, so I wonder what the advantage of multiple clocks is over using a "single-clock" model like the topos of trees and the $\square$ modality? The only paper I have seen advocate for the $\square$ modality is [Gratzer, Cavallo, Kavvos, Guatto & Birkedal, TOCL 2022](https://dl.acm.org/doi/10.1145/3514241) but there it is just a small example.

**Tags:** type-theory, dependent-type, ct.category-theory, step-indexing, guarded-domain-theory

> **Comments:**
> **username_1**: I am not exactly well-versed in models of guarded type theories, but the discussion at https://www.cs.cmu.edu/~rwh/papers/guarded/lics.pdf Guarded computational type theory, sections causality and then "Programming applications" just before section 1.1 motivates why the clocks were introduced. I am not sure, (it might be interesting to check) if the TOCL 2022 paper admits the "drop every second element" program without adding clocks.  
> **username_0**: Your example should work fine with $\square$ in that $\square \triangleright A \cong \square A$ holds which is the key property that clock quantification has that makes it work.  
> **username_2**: So actually a few of our papers have advocated for $\Box$ and $\rhd$ as the desirable primitives (the MTT papers actually use this as a motivating example, and the journal version at LMCS gives a rather long series of examples in this framework). My recollection is that $\Box$ was suggested in Clouston et al 2015 (Programming and Reasoning with Guarded Recursion for Coinductive Types). The main advantage of $\Box$ is conceptual simplicity: the same intended model, just one additional modality. The disadvantages are twofold: $\Box$ is much harder to handle proof-theoretically than clocks ....  
> **username_2**: ... and when one handles _nested_ guarded/coinductive types things become difficult: in order to even form $\Box \mathsf{Stream}(A)$ one needs to ensure that $A$ is constant, etc. In practice, I think it's mostly the former that wins out. To my knowledge, MTT was the first type theory which could handle both $\Box$ and $\rhd$ together, and that came out in 2020. On the other hand, clocked type theory and clocks in general are significantly easier to get off the ground syntactically... with the cost of far more complex semantics.  
> **username_0**: "the former that wins out" the former meaning what here? Clocks?  
> **username_2**: Ah sorry, I actually meant that one of the driving advantages of clocks has been that they were more easily shown to be syntactically feasible. Even though there are advantages with having multiple clocks etc, I think that the most important factor has just been that $\Box$ and $\rhd$ together was a bit thorny.  
> **username_0**: Ok I think that's a good answer: Historically it's because clock-based systems were easier to define based on our understanding of modal type theory. And objectively it's less clear but nesting of recursive types is trickier.  

---

## 0 answers

