そうそう、セルに型が付くのだった。セルに型フィールドと値フィールドがある。
特定番地のセルのフィールドに値が入っていることを
$`\quad \text{A2.Val} = 7\\
\quad \text{A2.Typ} = {\bf N}
%`$
まとめて
$`\quad \text{A2} = (7 : {\bf Nat})`$
次の機能がある。
- 型推論
- 明示的な型の指定
- 明示的型指定による型チェック
- 型指定の自動化
ガジェット設定の例
$`\quad \text{A1.Typ} = X\\
\quad \text{A1.Val} = ?\\
\quad \text{B1.Typ} = Y\\
\quad \text{B1.Val} = f(\text{A1.Val})\\
\quad \text{A2.Typ} = F(\text{A1.Val})\\
\quad \text{A2.Val} = \varphi_{\text{A.1.Val}}(\text{B2.Val})\\
\quad \text{B2.Typ} = G(\text{B1.Val}) \\
\quad \text{B2.Val} = ?
%`$
A1.Val と B2.Val がユーザー入力で、A2.Val が計算結果。
