宣言のみからなるテレスコープ〈依存レコード | 指標〉を純コンテキストと呼ぶことにする。宣言と割り当てが混じったコンテキストを混合コンテキストと呼ぶ。
純コンテキスト〈指標〉のあいだの手続きは多型判断〈poly-typejudgement〉と言ってもよい。
次が予想される。
- 純コンテキストのあいだの多型判断は、混合コンテキストと同値である。
さらに：
- 純コンテキストのあいだの多型判断から混合コンテキストへの変換はパッキング
- 混合コンテキストから純コンテキストへの変換はアンパッキング
次の記法を使う。$`\newcommand{\ARE}{ \mathrel{\hat{:} } }% elements are Types
\newcommand{\BEEQ}{ \mathrel{\hat{:=} } }% be equal
\newcommand{\EQBE}{ \mathrel{\hat{=:} } }% equal be
`$
- $`\vec{x} \ARE \vec{\alpha}`$ 多宣言＝指標＝純コンテキスト＝テレスコープ
- $`\vec{y} \BEEQ \vec{t}`$ 多割り当て＝手続き
- $`\vec{t} \EQBE \vec{y}`$ 多割り当て＝手続き（方向だけ変更）
手続きの完全な記述は：
$`\quad (\vec{y}\BEEQ \vec{t}) :\; \vec{x}\ARE \vec{\alpha} \vdash \vec{y}\ARE\vec{\beta}`$
名前を付けると：
$`\text{procedure }p :\; \vec{x}\ARE \vec{\alpha} \vdash \vec{y}\ARE\vec{\beta} \;\{\\
\quad \vec{y}\BEEQ \vec{t}\\
\}`$
あるいは：
$`\text{decl }p :\; \vec{x}\ARE \vec{\alpha} \vdash \vec{y}\ARE\vec{\beta}\\
\text{assig }p := \{\vec{y}\BEEQ \vec{t}\}
`$
あとの問題は、
- 指標のパラメータ化
- 帰納的型
- 組織化・編成・命名
- 散文化〈prosify〉
