名前〈ラベル〉と型項のペアを型宣言、あるいは単に宣言と呼ぶ。型項は判断のパック形式〈packed form〉のことがある。したがった、判断も宣言にエンコード〈パッキング〉できる。
宣言＝型宣言を束縛子ということもある。名前を型に束縛するから。しかし、名前を値に束縛する割り当て〈assignment〉も束縛子とも呼ぶ。
- 型束縛子〈型バインダー〉： 名前〈ラベル〉と型項のペア
- 値束縛子〈値バインダー〉： 名前〈ラベル〉と値項＝計算項のペア
型束縛子と値束縛子の依存タプル／依存レコードがコンテキストだが、コンテキストは引数リストやライブラリ／パッケージ形式にも使える。指標もコンテキストと思える。また、テレスコープとコンテキストは同義だと思ってもよい。
公平〈unbaiased〉なテレスコープ＝コンテキストをカリー化することができる。プログラミング言語の実装は、テレスコープを直接扱うことは出来なくて、カリー化のパック形式が使われる。
- アンカリー化したテレスコープ／判断は概念的
- カリー化したパック形式は実装
- 表層構文上は、テレスコープを空白区切りリストで表現できる。
- コンテキスト内の宣言と、ステージ上の判断の相互変換（パックとアンパック）が重要だが、暗黙化される。
宣言だけからなるテレスコープと指標は同義。テレスコープは通常、判断のコンテキスト側に使うが、ターゲットにテレスコープを許す。ターゲットにもテレスコープを許した質問の答〈アンサー | ソリューション〉は手続き項。
手続き項は手続きのボディにある。手続き自体は、ターゲットにテレスコープを許したフル判断〈項を入れた判断〉になる。
テレスコープ＝指標を多少とした圏ができるが、複圏／多圏でないと定式化できない。意味論はグロタンディーク・ファイブレーション。
なお、テレスコープは $`\vec{x} \hat{:} \vec{T}`$ と書く。$`\vec{x}, \vec{T}`$ は、同じインデックスセット $`I`$ を持つラベルベクトルと型項ベクトル。次の形に展開される。
- $`(x_i : T_i)_{i\in I} = (x_1 : T_1, \cdots, x_n : T_n)`$
テレスコープを含む判断は：
- $`\Gamma, \vec{x} \hat{:} \vec{T} \vdash!\; \vec{y} \hat{:}\vec{S}`$
- $`\Gamma, \vec{x} \hat{:} \vec{T} \vdash \vec{y} \;\widehat{:=}\; \vec{t} \hat{:}\vec{S}`$
