Functions from codata are not necessarily codata.

codata.hs

import qualified Data.Searchable as S   -- from infinite-search package
import Control.Applicative (liftA2)
import Data.Function (fix)

-- We will see that a function which takes codata as an argument is
-- not necessarily codata itself.  Here we see an isomorphism between
-- total functions of type (Stream Bool -> a) and finite trees of the
-- shape (SBFunc a) (below), whenever a has decidable equality.

-- We will be using infinite lists as streams, pretending
-- that nil isn't a thing (just to make it easier to work with them).
type Stream = []

-- A data structure reifying functions (Stream Bool -> a)
data SBFunc a
    -- depends on 0th bit (false, true)
    = Dep (SBFunc a) (SBFunc a)
    -- does not depend on 0th bit
    | NDep (SBFunc a)
    -- does not depend on any bits
    | Const a
    deriving (Show, Eq)

-- A searchable domain for Streams.
sb :: S.Set (Stream Bool)
sb = liftA2 (:) (S.doubleton False True) sb

-- Converts a total (Stream Bool -> a) function into a finite SBFunc.
toSBFunc :: (Eq a) => (Stream Bool -> a) -> SBFunc a
toSBFunc f
    | S.forevery sb $ \s -> S.forevery sb $ \s' -> f s == f s'
        = Const (f (fix (False :)))
    | S.forsome sb $ \s -> f (False : s) /= f (True : s)
        = Dep (toSBFunc (f . (False :))) (toSBFunc (f . (True :)))
    | otherwise
        = NDep (toSBFunc (f . (False :)))

fromSBFunc :: SBFunc a -> Stream Bool -> a
fromSBFunc (Dep f _) (False : s) = fromSBFunc f s
fromSBFunc (Dep _ t) (True  : s) = fromSBFunc t s
fromSBFunc (NDep r)  (_     : s) = fromSBFunc r s
fromSBFunc (Const x) _           = x

-- Check that this really is an isomorphism for a given function.
checkIso1 :: (Eq a) => (Stream Bool -> a) -> Bool
checkIso1 f = S.forevery sb (\s -> f s == conv s)
    where
    conv = fromSBFunc (toSBFunc f)

-- And for a given tree.
checkIso2 :: (Eq a) => SBFunc a -> Bool
checkIso2 sbfunc = sbfunc == toSBFunc (fromSBFunc sbfunc)


-- a few example functions
fourthBit :: Stream Bool -> Bool
fourthBit s = s !! 4

countTrues :: Int -> Stream Bool -> Int
countTrues n = length . filter id . take n

countFalses :: Int -> Stream Bool -> Int
countFalses n = length . filter not . take n

-- Two different ways of expressing countTrues. They will compare equal.
checkCount :: Int -> Bool
checkCount n = toSBFunc (countTrues n) == toSBFunc (countFalses n . map not)