データ型のSort

Agda 備忘

これまで誤解していたが、Agda2のdata typeの型の定義で、

  • (n : Nat) -> TermSeq n -> Set みたいな定義はよくて（ちなみに TermSeq nは長さがnのTermの列）、
  • (n : Nat) -> Term -> Pred (n-1) （ただし Pred 0 = Set） みたいな定義は不可能だ

ということをKtさんに教えてもらう。最後のrangeが明示的にSort (Setなど)になっていないとタイプチェックをクリアしないそうだ。だから、これまで悩んでいたエラーメッセージ「dataの型がSortではないのでParse エラーです」は「評価結果が構文的にSortになっていません」と解釈するべきだそうで。
あとついでに、Postulateした関数にはパターン・マッチングが使えず、マッチングを使うためにはデータ型にしなければならないそうだ。
というわけで、プログラムの書き直しが決まった。