2
$\begingroup$

The main purpose of clocks in guarded type theories (originating in Atkey & McBride ICFP 2013) 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 but there it is just a small example.

Improve this question
$\endgroup$
7
  • $\begingroup$ I am not exactly well-versed in models of guarded type theories, but the discussion at 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. $\endgroup$
    – Ilk
    Aug 9, 2022 at 1:23
  • 1
    $\begingroup$ 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. $\endgroup$
    – Max New
    Aug 9, 2022 at 11:12
  • 2
    $\begingroup$ 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 .... $\endgroup$
    – daniel gratzer
    Aug 11, 2022 at 17:15
  • 2
    $\begingroup$ ... 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. $\endgroup$
    – daniel gratzer
    Aug 11, 2022 at 17:18
  • 1
    $\begingroup$ 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. $\endgroup$
    – Max New
    Aug 12, 2022 at 13:53

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.