Overview

Guarded types were first introduced by Nakano [0] in an STLC with recursive types and subtyping such that the following hold (using the modern ⊳ notation):

A ≼ ⊳A
A → B ≼ ⊳A → ⊳B ≼ ⊳(A → B)

Modern type systems present the guarded modality as an applicative functor instead (laws omitted below), together with a guarded fixpoint operator:

next : A → ⊳A
ap : ⊳(A → B) → ⊳A → ⊳B

dfix : (⊳A → A) → ⊳A
dfix f ≃ next (f (dfix f))

fix : (⊳A → A) → A
fix f ≝ f (dfix f) -- ≃ f (next (fix f))

Given some endofunctor F on types, μ(F ∘ ⊳) is a fixpoint of F ∘ ⊳; the anamorphism is defined through fix. We then have the tools for programming with guarded recursive types μ(F ∘ ⊳). Birkdeal, Møgelberg, Schwinghammer, and Stovring [1] present a model of guarded dependent type theory, then providing the tools for proving with guarded recursive types.

To coprogram with coinductive types, Atkey and McBride [2] index the modality and the above constructs by a clock κ, and show that νF ≝ ∀κ. μ(F ∘ ⊳ᴷ) is a cofixpoint of F. Concretely, for example, μX. A × ⊳X is the type of guarded streams of A, while ∀κ. μX. A × ⊳ᴷX is the type of coinductive streams of A. This system additionally requires that F commute with clock quantification (which can be shown metatheoretically for strictly positive functors F), as well as a construct that permits immediately “running” a clock that was just quantified.

force : (∀κ. ⊳ᴷA) → (∀κ. A)

This system disallows instantiating a clock quantification using a clock that’s free in the type, which

disallows us from using the same clock variable twice, preventing multiple “time-streams” from becoming conflated

but Bizjak and Møgelberg [5] remove this restriction by giving a model in which two clocks can be “synchronized”.

Birkedal and Møgelberg [3] show that in a dependently-typed system, guarded recursive types can be defined as guarded recursive functions on types, and Møgelberg [4] shows that coinductive types can be too using clock quantification. More precisely, since fix can act on types, the cofixpoint type itself can be defined in terms of it too:

▸ᴷ : ⊳ᴷ𝒰 → 𝒰
▸ᴷ (nextᴷ A) ≃ ⊳ᴷA

νF ≝ ∀κ. fixᴷ (F ∘ ▸ᴷ)
νF ≃ F νF

These dependent type theories provide the following distributive law of modalities over dependent functions:

d : ⊳((x : A) → B) → (x : A) → ⊳B
d (nextᴷ f) ≃ nextᴷ ∘ f

This isn’t the corresponding notion of ap for dependent functions, but given a function f : ⊳((x : A) → B) and an argument x : ⊳A, what would the type of the application of f to x be? Bizjak, Grathwohl, Clouston, Møgelberg, and Birkedal [6] resolve this issue with a notion of delayed substitution in their Guarded Dependent Type Theory (GDTT), which waits for x to reduce to next a to substitute into B.

Alternatively, and apparently more popularly, Bahr, Grathwohl, and Møgelberg [7] introduce a notion of ticks, which are inhabitants of clocks, in their Clocked Type Theory (CloTT). Notably, the ticked modality acts like quantification over ticks, and CloTT provides reduction semantics to guarded types and guarded fixpoints. The postulated constructs of guarded type theory can be implemented using ticks, and there is a special ⬦ that can be applied to ticks whose clock isn’t used elsewhere in the context.

next : ∀κ. A → ⊳(α : κ). A
nextᴷ a _ ≝ a

ap : ∀κ. ⊳(α : κ).(A → B) → ⊳(α : κ).A → ⊳(α : κ).B
apᴷ f a α ≝ (f α) (a α)

dfix : ∀κ. (⊳(α : κ).A → A) → ⊳(α : κ).A
dfixᴷ f ⬦ ⇝ f (dfixᴷ f)

fix : (⊳(α : κ).A → A) → A
fixᴷ f ≝ f (dfixᴷ f)

▸ᴷ : ⊳(α : κ).𝒰 → 𝒰
▸ᴷ A ≝ ⊳(α : κ).(A α)

force : (∀κ. ⊳(α : κ).A) → (∀κ. A)
force f κ ≝ f κ ⬦

There is still one significant deficiency in the guarded type theories so far: reasoning about bisimulation using the usual identity type remains difficult. Recently, there has been a trend of augmenting guarded type theories with cubical path types (or rather, augmenting cubical type theory with guarded types): Guarded Cubical Type Theory (GCTT) [8] is a cubical variant of GDTT, Ticked Cubical Type Theory (TCTT) [9] is a cubical variant of CloTT without clock quantification, and Clocked Cubical Type Theory (CCTT) [10] is a cubical variant of CloTT with clock quantification. In all of these, the cubical path type corresponds to bisimilarity of guarded recursive types and guarded coinductive types. Alternatively, McBride [11] shows that observational equality can also implement bisimilarity.

Theses and Dissertations

There have been several theses and dissertations on the topic of guarded types that deserve mentioning, some of which cover some of the papers already mentioned above. The following are just the ones I know of.

Vezzosi’s licentiate thesis [12] collects together two separate works. The first is a mechanized proof of strong normalization of a simply-typed variant of Birkedal and Møgelberg’s system [3]. The second extends a clocked, guarded dependent type theory by defining a well-order on clocks (which they call Times) and additionally adds existential quantification to enable encoding inductive types. In fact, the system resembles sized types more than it does guarded types, save for the fact that inductives and coinductives are still encoded as existentially and universally clock-quantified guarded fixpoints. Because in sized types, fixpoints only reduce when applied to inductive constructor head forms, it’s unclear to me how reduction in their system behaves. Finally, just as in my own thesis, they note that to encode arbitrarily-branching inductive types, a limit operator on Time is required, which continue to believe would render the order undecidable.

Grathwohl’s PhD dissertation [13] mainly deals with GDTT and GCTT. It also includes the guarded λ-calculus from an earlier paper, which adds to a guarded STLC a second modal box operator that acts like Atkey and McBride’s clock quantification [2] but as if there is only ever one clock. The dissertation ends with an alternative to GDTT that appears to be an early variant of CloTT.

Bizjak’s PhD dissertation [14] also includes GDTT as well as the same guarded λ-calculus. It provides two different models of guarded types, one of which is the model for clock synchronization [5], and gives applications to modelling System F with recursive types and nondeterminism.

Paviotti’s doctoral thesis [15] is an application of GDTT in synthetic guarded domain theory to give denotation semantics to PCF (which includes the Y combinator) and FPC (which includes recursive types).

References

[0] Nakano, Hiroshi. A Modality for Recursion. (LICS 2000). ᴅᴏɪ:10.1109/lics.2000.855774.
[1] Birkedal, Lars; Møgelberg, Rasmus Ejlers; Schwinghammer, Jans; Stovring, Kristian. First Steps in Synthetic Guarded Domain Theory: .Step-Indexing in the Topos of Trees. (LICS 2011). ᴅᴏɪ:10.1109/LICS.2011.16.
[2] Atkey, Robert; McBride, Conor. Productive Coprogramming with Guarded Recursion. (ICFP 2013). ᴅᴏɪ:10.1145/2500365.2500597.
[3] Birkedal, Lars; Møgelberg, Rasmus Ejlers. Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. (LICS 2013). ᴅᴏɪ:10.1109/LICS.2013.27.
[4] Møgelberg, Rasmus Ejlers. A type theory for productive coprogramming via guarded recursion. (LICS 2014). ᴅᴏɪ:10.1145/2603088.2603132.
[5] Bizjak, Aleš; Møgelberg, Rasmus Ejlers. A Model of Guarded Recursion With Clock Synchronisation. (MFPS 2015). ᴅᴏɪ:10.1016/j.entcs.2015.12.007.
[6] Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus Ejlers; Birkedal, Lars. Guarded Dependent Type Theory with Coinductive Types. (FoSSaCS 2016). ᴅᴏɪ:10.1007/978-3-662-49630-5_2.
[7] Bahr, Patrick; Grathwohl, Hans Bugge; Møgelberg, Rasmus Ejlers. The Clocks Are Ticking: No More Delays! (LICS 2017). ᴅᴏɪ:10.1109/LICS.2017.8005097.
[8] Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea. Guarded Cubical Type Theory. (Journal of Automated Reasoning, 2019). ᴅᴏɪ:10.1007/s10817-018-9471-7.
[9] Møgelberg, Rasmus Ejlers; Veltri, Niccolò. Bisimulation as Path Type for Guarded Recursive Types. (POPL 2019). ᴅᴏɪ:10.1145/3290317.
[10] Kristensen, Magnus Baunsgaard; Møgelberg, Rasmus Ejlers; Vezzosi, Andrea. Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks. (LICS 2022). ᴅᴏɪ:10.1145/3531130.3533359.
[11] McBride, Conor. Let’s see how things unfold: reconciling the infinite with the intensional. (CALCO 2009). ᴅᴏɪ:10.1007/978-3-642-03741-2_9.
[12] Vezzosi, Andrea. Guarded Recursive Types in Type Theory. (Licentiate thesis, 2015). https://saizan.github.io/vezzosi-lic.pdf.
[13] Grathwohl, Hans Bugge. Guarded Recursive Type Theory. (PhD dissertation, 2016). https://hansbugge.dk/pdfs/phdthesis.pdf.
[14] Bizjak, Aleš. On Semantics and Applications of Guarded Recursion. (PhD dissertation, 2016). https://abizjak.github.io/documents/thesis/semantics-applications-gr.pdf.
[15] Paviotti, Marco. Denotational semantics in Synthetic Guarded Domain Theory. (Doctoral thesis, 2016). https://mpaviotti.github.io/assets/papers/paviotti-phdthesis.pdf.