[Agda] Data.Thunk, cofix question

[William Harrison]

Thanks again — was/is there a musical notation formulation of cofix? 

Bill

> On May 11, 2020, at 10:57 AM, Nils Anders Danielsson <nad at cse.gu.se> wrote:
> 
> 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