Notes on Guarded Types:
A Short Lit Review


Work Summary
Nakano1 STLC + recursive types + guarded types
Birkdeal, Møgelberg, Schwinghammer, Stovring2 dependent types + recursive types + guarded types
Atkey and McBride3 STLC + recursive types + guarded types + clocks
Birkedal and Møgelberg4 dependent types + guarded types
Møgelberg5 dependent types + guarded types + clocks
GDTT6 dependent types + guarded types + clocks + delayed substitution
CloTT7 dependent types + guarded types + ticks + clocks
GCTT8 cubical type theory + guarded types + delayed substitution
TCTT9 cubical type theory + guarded types + ticks
CCTT10 cubical type theory + guarded types + ticks + clocks

Guarded types were first introduced by Nakano1 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 Stovring2 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 McBride3 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øgelberg11 remove this restriction by giving a model in which two clocks can be “synchronized”.

Birkedal and Møgelberg4 show that in a dependently-typed system, guarded recursive types can be defined as guarded recursive functions on types, and Møgelberg5 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øgelberg7 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, McBride12 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 thesis13 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 system4. 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 dissertation14 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 quantification3 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 dissertation15 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 synchronization11, and gives applications to modelling System F with recursive types and nondeterminism.

Paviotti’s doctoral thesis16 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).

  1. Nakano, Hiroshi. A Modality for Recursion. (LICS 2000). ᴅᴏɪ: 10.1109/lics.2000.855774 2

  2. 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

  3. Atkey, Robert; McBride, Conor. Productive Coprogramming with Guarded Recursion. (ICFP 2013). ᴅᴏɪ: 10.1145/2500365.2500597 2 3

  4. 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 2 3

  5. Møgelberg, Rasmus Ejlers. A type theory for productive coprogramming via guarded recursion. (LICS 2014). ᴅᴏɪ: 10.1145/2603088.2603132 2

  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 2

  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 2

  9. Møgelberg, Rasmus Ejlers; Veltri, Niccolò. Bisimulation as Path Type for Guarded Recursive Types. (POPL 2019). ᴅᴏɪ: 10.1145/3290317 2

  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 2

  11. Bizjak, Aleš; Møgelberg, Rasmus Ejlers. A Model of Guarded Recursion With Clock Synchronisation. (MFPS 2015). ᴅᴏɪ: 10.1016/j.entcs.2015.12.007 2

  12. McBride, Conor. Let’s see how things unfold: reconciling the infinite with the intensional. (CALCO 2009). ᴅᴏɪ: 10.1007/978-3-642-03741-2_9

  13. Vezzosi, Andrea. Guarded Recursive Types in Type Theory. (Licentiate thesis, 2015). ᴜʀʟ:

  14. Grathwohl, Hans Bugge. Guarded Recursive Type Theory. (PhD dissertation, 2016). ᴜʀʟ:

  15. Bizjak, Aleš. On Semantics and Applications of Guarded Recursion. (PhD dissertation, 2016). ᴜʀʟ:

  16. Paviotti, Marco. Denotational semantics in Synthetic Guarded Domain Theory. (Doctoral thesis, 2016). ᴜʀʟ: