@@ -685,6 +685,95 @@ without any explicit use of ``Force`` or ``Delay``:
685685 ifThenElse True t e = t;
686686 ifThenElse False t e = e;
687687
688+Codata Types
689+============
690+
691+Codata types are like regular data types, except that they allow for us to
692+define infinite data structures. More precisely, for a type ``T``, each of its
693+constructor arguments of type ``T`` are transformed into a coinductive parameter
694+``Inf T``. This makes each of the ``T`` arguments lazy, and allows infinite data
695+structures of type ``T`` to be built. One example of a codata type is Stream,
696+which is defined as follows.
697+
698+.. code-block:: idris
699+
700+ codata Stream : Type -> Type where
701+ (::) : (e : a) -> Stream a -> Stream a
702+
703+This gets translated into the following by the compiler.
704+
705+.. code-block:: idris
706+
707+ data Stream : Type -> Type where
708+ (::) : (e : a) -> Inf (Stream a) -> Stream a
709+
710+The following is an example of how the codata type ``Stream`` can be used to
711+form an infinite data structure. In this case we are creating an infinite stream
712+of ones.
713+
714+.. code-block:: idris
715+
716+ ones :: Stream Nat
717+ ones = 1 :: ones
718+
719+It is important to note that codata does not allow the creation of infinite
720+mutually recursive data structures. For example the following will create an
721+infinite loop and cause a stack overflow.
722+
723+.. code-block:: idris
724+
725+ mutual
726+ codata Blue a = B a (Red a)
727+ codata Red a = R a (Blue a)
728+
729+ mutual
730+ blue : Blue Nat
731+ blue = B 1 red
732+
733+ red : Red Nat
734+ red = R 1 blue
735+
736+ mutual
737+ findB : (a -> Bool) -> Blue a -> a
738+ findB f (B x r) = if f x then x else findR f r
739+
740+ findR : (a -> Bool) -> Red a -> a
741+ findR f (R x b) = if f x then x else findB f b
742+
743+ main : IO ()
744+ main = do printLn $ findB (== 1) blue
745+
746+To fix this we must add explicit ``Inf`` declarations to the constructor
747+parameter types, since codata will not add it to constructor parameters of a
748+**different** type from the one being defined. For example, the following
749+outputs "1".
750+
751+.. code-block:: idris
752+
753+ mutual
754+ data Blue : Type -> Type where
755+ B : a -> Inf (Red a) -> Blue a
756+
757+ data Red : Type -> Type where
758+ R : a -> Inf (Blue a) -> Red a
759+
760+ mutual
761+ blue : Blue Nat
762+ blue = B 1 red
763+
764+ red : Red Nat
765+ red = R 1 blue
766+
767+ mutual
768+ findB : (a -> Bool) -> Blue a -> a
769+ findB f (B x r) = if f x then x else findR f r
770+
771+ findR : (a -> Bool) -> Red a -> a
772+ findR f (R x b) = if f x then x else findB f b
773+
774+ main : IO ()
775+ main = do printLn $ findB (== 1) blue
776+
688777Useful Data Types
689778=================
690779