2013-02-12から1日間の記事一覧

Idrisで無限ストリーム

codataを使うと、無限ストリームが作れる。codata型のコンストラクターは遅延評価され、またcodata型を返す関数はコンパイル時に簡約されない。 module Main codata Stream a = (::) a (Stream a) iterate : (a -> a) -> a -> Stream a iterate f a = iterat…