Idrisで無限ストリーム

codataを使うと、無限ストリームが作れる。codata型のコンストラクターは遅延評価され、またcodata型を返す関数はコンパイル時に簡約されない。

module Main

codata Stream a = (::) a (Stream a)

iterate : (a -> a) -> a -> Stream a
iterate f a = iterate' a
  where
    iterate' a = a :: iterate' (f a)

take : Nat -> Stream a -> List a
take O _ = []
take (S n) (x :: xs) = x :: take n xs

natStr : Stream Nat
natStr = iterate S O

main : IO ()
main = print (take 10 natStr)

実行してみる。

$ idris -o stream stream.idr --total --warnpartial
stream.idr:8:Warning - Main.iterate.0.#iterate' is possibly not total due to recursive path Main.iterate.0.#iterate' --> Main.iterate.0.#iterate'
$ ./stream 
[O, sO, ssO, sssO, ssssO, sssssO, ssssssO, sssssssO, ssssssssO, sssssssssO]
$ 

追記: .ibcファイルが残っていると、警告が表示されない。
さらに追記: iterateの定義を次のように変更すると、警告は出なくなる。

iterate f a = a :: iterate f (f a)

codataをdataに書き換えると、コンパイルに失敗する。

$ idris -o badstream badstream.idr --total --warnpartial
badstream.idr:8:Warning - Main.iterate.0.#iterate' is possibly not total due to recursive path Main.iterate.0.#iterate' --> Main.iterate.0.#iterate'
badstream.idr:6:Main.iterate is possibly not total due to: Main.iterate.0.#iterate'

ただし、オプションに--totalを指定しないとコンパイルが通るので注意すること。そのまま実行するとSegmentation faultで落ちる。

$ idris -o badstream badstream.idr --warnpartial
badstream.idr:8:Warning - Main.iterate.0.#iterate' is possibly not total due to recursive path Main.iterate.0.#iterate' --> Main.iterate.0.#iterate'
badstream.idr:6:Warning - Main.iterate is possibly not total due to: Main.iterate.0.#iterate'
badstream.idr:15:Warning - Main.natStr is possibly not total due to: Main.iterate.0.#iterate'
badstream.idr:18:Warning - Main.main is possibly not total due to: Main.iterate.0.#iterate'
$ ./badstream 
Segmentation fault (コアダンプ)
$