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 (コアダンプ) $
