[Agda] Question about colists, musical notation vs coinductive records, and all that

[James Wood]

In the standard library, `nothing` and `just` are in lowercase. The
change should fix that issue.

James

On 29/04/2020 20:20, Eric Finster wrote:
> I used my own Maybe type because I didn't have the standard library
> handy. I guess I named the constructors differently?
> 
> On Wed, Apr 29, 2020, 21:08 William Harrison
> <william.lawrence.harrison at gmail.com
> <mailto:william.lawrence.harrison at gmail.com>> wrote:
> 
>     Thank you Eric and Guillaume! I think you have both answered my
>     questions, and the pointer to Cowriter are spot on.
> 
>     Eric,
> 
>     What you wrote is what I was trying to write, although I get an odd
>     syntax error when I try it (I’ve attached the file that generates
>     the error). It is possible that this is just a stupid mistake on my
>     part made after staring at an emacs buffer all day.
> 
>     This definition:
>     iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
>     Hd (iterate1 {A} f a) = Just (a , loop (f a))
>        where
>          loop : Maybe A → Colist A
>          loop Nothing   = hd Nothing
>          loop (Just a') = iterate1 f a’
> 
>     Generates this error:
> 
>     …/ColistQuestion.agda:19,6-20
>     Could not parse the left-hand side loop (Just a')
>     Operators used in the grammar:
>       None
>     when scope checking the left-hand side loop (Just a') in the
>     definition of loop
> 
>     Am I missing something obvious?
> 
>     Thanks Again,
>     Bill
> 
>>     On Apr 29, 2020, at 2:53 PM, Guillaume Allais
>>     <guillaume.allais at ens-lyon.org
>>     <mailto:guillaume.allais at ens-lyon.org>> wrote:
>>
>>     Hi William,
>>
>>     In the standard library we use a notion of `Thunk` for sized codata.
>>     This gives you definitions that look essentially like the ones using
>>     musical notations but on which you can define more compositional
>>     operations thanks to sized types.
>>
>>     You can find colist here:
>>     http://agda.github.io/agda-stdlib/Codata.Colist.html
>>     <https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fagda.github.io%2Fagda-stdlib%2FCodata.Colist.html&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C15aff5a127f64909316608d7ec725c10%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637237848229682364&sdata=sZz8w3FzAvZpRId8eV3QNHTWPXm50DqpGcIIfSJq2S8%3D&reserved=0>
>>
>>     And what you call transcript corresponds to our cowriter:
>>     http://agda.github.io/agda-stdlib/Codata.Cowriter.html
>>     <https://eur02.safelinks.protection.outlook.com/?url=http%3A%2F%2Fagda.github.io%2Fagda-stdlib%2FCodata.Cowriter.html&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C15aff5a127f64909316608d7ec725c10%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637237848229692356&sdata=%2FVkDvcHLa2EHA65ufOZ33sim%2BdbjeJWUQapxMiCOF7M%3D&reserved=0>
>>
>>     Both come with various functions, including an `unfold` one that is
>>     a generalisation of your `iterate` where we distinguish between the
>>     type of the internal state and the type of the values outputted in
>>     the codatatype.
>>
>>     Best,
>>     guillaume
>>
>>
>>     On 29/04/2020 17:58, William Harrison wrote:
>>>     Hi-
>>>
>>>     I have a question about the best way to handle colists — aka,
>>>     potentially infinite lists as opposed to streams — in Agda. I
>>>     give some examples below in Haskell and Agda, and I’ve also
>>>     attached *.hs and *.agda files with complete, stand-alone
>>>     definitions.
>>>
>>>     In Haskell, the built-in iterate function always produces an
>>>     infinite list:
>>>
>>>     iterate :: (a -> a) -> a -> [a]
>>>     iterate f a =  a : iterate f (f a)
>>>
>>>     This can be represented in Agda using a Stream (defined as a
>>>     coinductive record):
>>>
>>>     iterate : ∀ {a} → (a → a) → a → Stream a
>>>     hd (iterate f a) = a
>>>     tl (iterate f a) = iterate f (f a)
>>>
>>>     Now, back in Haskell, we can define a *potentially* infinite list
>>>     by introducing Maybe in the codomain of f:
>>>
>>>     iterate1 :: (a -> Maybe a) -> a -> [a]
>>>     iterate1 f a = a : case f a of
>>>                            Just a1 -> iterate1 f a1
>>>                            Nothing -> []
>>>
>>>     Using the musical notation for coinduction in Agda, I can get
>>>     something similar:
>>>
>>>     data Colist (A : Set) : Set where
>>>      []  : Colist A
>>>      _∷_ : A → (∞ (Colist A)) → Colist A  
>>>
>>>     iterate1 : ∀ {a} → (a → Maybe a) → a → Colist a
>>>     iterate1 f a = a ∷ ♯ (case f a of
>>>                           λ { (just a₁) → (iterate1 f a₁)
>>>                             ; nothing   → []
>>>                             })
>>>
>>>     My question is, how do I use coinductive records to define Colist
>>>     rather than musical notation. Is there a standard approach? That
>>>     isn’t clear. I'm supposing that musical notation should be avoided.
>>>
>>>     What I’m really trying to define is analogous functions to
>>>     iterate for what I’ll call the transcript data type, defined
>>>     below in Haskell and Agda:
>>>
>>>     data T e a = e :<< T e a | V a — a "transcript"; like a list with
>>>     an "answer"
>>>
>>>     data T (e : Set) (a : Set) : Set where
>>>       V    : a → T e a
>>>       _<<_ : e → ∞ (T e a) → T e a
>>>
>>>     All these definitions are given in the attached files.
>>>
>>>     Thanks!
>>>     Bill
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>     _______________________________________________
>>>     Agda mailing list
>>>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>>     https://lists.chalmers.se/mailman/listinfo/agda
>>>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C15aff5a127f64909316608d7ec725c10%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637237848229692356&sdata=k9hH1BLwqm4QhVy%2F4iknx8zp9pdCR9DCxlHAxAdiTwE%3D&reserved=0>
> 
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C15aff5a127f64909316608d7ec725c10%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637237848229702357&sdata=rzkhmQbw15yms%2B95hpMp2dvTw6esrCDMb03hpw3q%2FFg%3D&reserved=0>
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://eur02.safelinks.protection.outlook.com/?url=https%3A%2F%2Flists.chalmers.se%2Fmailman%2Flistinfo%2Fagda&data=02%7C01%7Cjames.wood.100%40strath.ac.uk%7C15aff5a127f64909316608d7ec725c10%7C631e0763153347eba5cd0457bee5944e%7C0%7C0%7C637237848229722342&sdata=eHNbaktehw%2Bq5B1%2FI6ANeEehIUQeFQC8hkwLwZ2gF4g%3D&reserved=0
>