Overview

Guarded types were first introduced by Nakano¹ 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² 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³ 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¹¹ remove this restriction by giving a model in which two clocks can be “synchronized”.

Birkedal and Møgelberg⁴ show that in a dependently-typed system, guarded recursive types can be defined as guarded recursive functions on types, and Møgelberg⁵ 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⁷ 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)⁸ is a cubical variant of GDTT, Ticked Cubical Type Theory (TCTT)⁹ is a cubical variant of CloTT without clock quantification, and Clocked Cubical Type Theory (CCTT)¹⁰ 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¹² 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¹³ 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⁴. 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¹⁴ 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³ 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¹⁵ 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¹¹, and gives applications to modelling System F with recursive types and nondeterminism.

Paviotti’s doctoral thesis¹⁶ 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).