Example of using a simple codata structure

number_line.idr

%default total

-- An infinite list of numbers (.., -2, -1, 0, 1, 2, ...)
-- with a way to go forward and backward.
codata NumberLine = NL Int NumberLine NumberLine

-- Make a number line starting at a particular point.
--
-- Try changing "codata" above into "data". This function will fail to compile
-- as it's not guaranteed to terminate.
makeNL : Int -> NumberLine
makeNL n = NL n (makeNL (n - 1)) (makeNL (n + 1))

-- Bunch of obvious accessors.

val : NumberLine -> Int
val (NL v _ _) = v

prev : NumberLine -> NumberLine
prev (NL _ p _) = p

next : NumberLine -> NumberLine
next (NL _ _ n) = n

-- The line may be infinite, but we can still recurse over it, as long as it's
-- bounded.
mulPrev : Nat -> NumberLine -> NumberLine
mulPrev Z l = l
mulPrev (S n) (NL _ p _) = mulPrev n p

-- However we can't recurse infinitely, this won't work.
-- Just try uncommenting it, Idris will not accept it.
{-
infPrev : NumberLine -> NumberLine
infPrev (NL _ p _) = infPrev p
-}

-- This doesn't work either, Idris is too smart to get caught.
{-
infPrev2 : Int -> NumberLine -> NumberLine
infPrev2 i n = if i > 0 then infPrev2 (i-1) (prev n) else n
-}

-- Higher order function, no problem at all. 
repeatedly : (a -> a) -> Nat -> a -> a
repeatedly f Z v = v
repeatedly f (S n) v = repeatedly f n (f v)

-- Putting it all together.
main : IO ()
main = do (print . val . mulPrev 2 . repeatedly prev 2 . next . makeNL) 3