[Agda] Data.Thunk, cofix question

[Nils Anders Danielsson]

On 2020-05-11 13:39, William Harrison wrote:
> For example, how would you define some simple Stream example with it
> (e.g., 'ones = 1 : ones’ in Haskell)?

Here's one way:

   {-# OPTIONS --sized-types #-}

   open import Codata.Stream
   open import Codata.Thunk
   open import Data.Nat

   ones : ∀ {i} → Stream ℕ i
   ones = cofix (Stream ℕ) (1 ∷_)

I'm not sure what the theoretical status of Thunk is, I seem to recall
that Andreas Abel expressed some skepticism towards this kind of
construction.

-- 
/NAD