Telescopes

A telescope is a non-empty sequence of variable bindings annotated by their types, with each variable surrounded by parentheses. For example, (x : Nat) (y : Bool) (z : Bool) is a telescope. Adjacent variables that have the same type can share a type annotation. For example, the same telescope can be written equivalently as (x : Nat) (y z : Bool). The type of each variable can depend on the previous variables in the telescope, for example (A : Set) (n : Nat) (v : Vec A n).

Note

The terminology is due to de Bruijn [1]: “The word was inspired, of course, by the old-fashioned instrument consisting of segments that slide one into another.” Each variable binding corresponds to a segment of the telescope, which can slide into (i.e. depend on) the previous ones.

Telescopes appear in the following parts of the Agda syntax:

postulate
  f : (A : Set) (n : Nat) (v : Vec A n) → Nat

data D (A : Set) (n : Nat) (v : Vec A n) : Set where
  -- ...

module M (A : Set) (n : Nat) (v : Vec A n) where
  -- ...

In telescopes of data and record types as well as parameterised modules, it is allowed to omit the type of a variable binding. This is equivalent to giving the variable the type _ (see implicit arguments).

data D' A n (v : Vec A n) : Set where
  -- ...

module M' A n (v : Vec A n) where
  -- ...

In function types, the type of a variable binding can be omitted if the module telescope starts with forall or ∀.

postulate
  f' : ∀ A n (v : Vec A n) → Nat

When binding a variable of a record type (but not a data type), it is possible to deconstruct the bound variable by pattern matching:

module N ((x , y) : Nat × Bool) where
  -- ...

Variable bindings in a telescope can be implicit or instance arguments. For example:

postulate
  mconcat : {A : Set} {{monoidA : Monoid A}} → List A → A

They can also be irrelevant or carry another modality. For example:

postulate
  div : (m n : Nat) .(nz : NonZero n) → Nat

Irrefutable Patterns in Binding Positions

Since Agda 2.6.1, irrefutable patterns can be used at every binding site in a telescope to take the bound value of record type apart. The type of the second projection out of a dependent pair will for instance naturally mention the value of the first projection. Its type can be defined directly using an irrefutable pattern as follows:

proj₂ : ((a , _) : Σ A B) → B a

And this second projection can be implemented with a lamba-abstraction using one of these irrefutable patterns taking the pair apart:

proj₂ = λ (_ , b) → b

Using an as-pattern makes it possible to name the argument and to take it apart at the same time. We can for instance prove that any pair is equal to the pairing of its first and second projections, a property commonly called eta-equality:

eta : (p@(a , b) : Σ A B) → p ≡ (a , b)
eta p = refl

Let Bindings in Telescopes

Telescopes of function types and parameterised modules (but not of data and record types) can also contain let bindings. When used in this manner, the let-binding should be surrounded by parentheses and the in part of the syntax is omitted. For example:

postulate
  g : (x : Nat) (let y = x + x) (v : Vec Nat y) → Nat

Let-bound variables in a module telescope are available in the whole module. For example:

module O (X : Set) (let LX = List X) (l : LX) where

  extend : LX → LX
  extend m = l ++ m

In general, any valid let-binding can also be used in a telescope. For example, it is possible to pattern match on a record type with a let-binding:

postulate
  h : (f : Nat → (Bool × Bool)) (let (x0 , y0) = f 0) (tx : IsTrue x0) → IsTrue y0

Another notable example is opening a module in a telescope:

module M1 (X : Set) (let open M X) where

This can also be written more compactly with just open (without the let):

module M2 (X : Set) (open M X) where

References

[1] N.G. de Bruijn. “Telescopic mappings in typed lambda calculus.” Information and Computation, Volume 91, Issue 2, 1991.