帰納と余帰納
制限された再帰
Idrisには函数が全域函数であるかチェックする機能があるのだけれども、プログラムに制限なく再帰が使われていると、その函数が値を返すのか、それとも停止しないで値が返らないままなのか判定する方法が存在し得ない。そこで、Idrisでは再帰呼び出しの引数の値が「減少」する場合にはその函数は停止する、そうでない場合には停止しないかもしれない、というように判定する。
再帰呼び出しの引数が「減少」するというのは、要はその函数が帰納的に定義されているということだ。引数が減少していけば、いつかは必ずベースケースに到達し、そこで計算は終了する。
帰納的データ型
data宣言によって導入されるデータ型も帰納的なデータ構造で、必ず有限の大きさになっている。
IdrisのListは次のように定義されている。
data List a = Nil | (::) a (List a)
IdrisのListはHaskellのListとは違い、無限リストにはならない。そのため、IdrisのPreludeにはiterate函数などは存在していない。
遅延評価
Haskellでは、評価戦略として遅延評価 lazy evaluation を採用しているが、Idrisは標準では先行評価 eager evaluation を行う。しかし、Idrisでも遅延評価を行うことはできる。
ifは手続き型プログラミングでは基本となる制御構造だが、函数プログラミングにおいては単なる函数に過ぎない。現にIdrisのif式は、boolElimという函数の呼び出しの糖衣構文である。
boolElim : Bool -> |(t : a) -> |(f : a) -> a boolElim True t e = t boolElim False t e = e syntax if [test] then [t] else [e] = boolElim test t e syntax [test] "?" [t] ":" [e] = if test then t else e
カルトゥーシュのようになっている |(t : a) といった記法は、その引数を遅延評価することを表す。もし遅延評価でなく、先行評価だとすると、boolElimの第1引数の真偽にかかわらず、引数tと引数fは必ず先に評価されることになってしまう。Idrisのように純粋関数型言語であって、しかも函数が必ず停止すると分かっている場合には、先行評価だろうと遅延評価だろうと結果には違いはないのだけれども、やはり評価する必要のない式を評価するのは全く無駄だ。そういうわけで、遅延評価にする。
