依存型と線形型を持つ

配列の境界検査ができるらしい

arrayref(T, I) という型を持つ

I は配列のサイズ

依存型の一種

静的に検査するので、実行時には検査しない

一方、普通の？言語では、静的に検査はできてないので実行時にやっている

Haskellとかでもたしかそう

Termination Analysisができるらしい

再帰関数の停止性検査をする

参考