Isomorphism between streams and function-of-Nat

NatStream.hs

{-# OPTIONS_GHC -Wall #-}
module NatStream where

data Nat = Zero | Succ Nat

data Stream a = a :< Stream a

-- Stream is the trie induced by Nat.
-- Here's the isomorphism, explicitly:

toFun :: Stream a -> (Nat -> a)
toFun (a :< _ ) Zero     = a
toFun (_ :< as) (Succ n) = toFun as n

toStream :: (Nat -> a) -> Stream a
toStream f = f Zero :< toStream (f . Succ)