技術の進歩

昨年11月の話の続報。
Agda2のdata typeの型の定義で、以下のようなデータ型 Predを定義しようとすると、「dataの型がSortではないのでParse エラーです」というエラーが出ると言う話を書いた。

• Pred 0 = Set
• Pred n+1 = D ->Pred n

ただし D: Set とする。
本日A君から聞いて判明したのだが、現在のバージョンでは型検査のアルゴリズムが進歩して、上の定義が可能になったようだ。たしかに、上の定義は非常に問題を起こさなそうに見えるので、型検査を通るようになったのはありがたい話だ。