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

[William Harrison]

This is just a follow-up question to my questions from last week about colists, mainly to check my understanding. Consider these typical definitions in Data.Colist that depend on Data.Thunk/sized types: 
[_] <http://agda.github.io/agda-stdlib/Codata.Colist.html#1830> : <> A <http://agda.github.io/agda-stdlib/Codata.Colist.html#1187> → <> Colist <http://agda.github.io/agda-stdlib/Codata.Colist.html#1245> A <http://agda.github.io/agda-stdlib/Codata.Colist.html#1187> ∞ <http://agda.github.io/agda-stdlib/Agda.Builtin.Size.html#302>
[ <http://agda.github.io/agda-stdlib/Codata.Colist.html#1830> a <http://agda.github.io/agda-stdlib/Codata.Colist.html#1853> ] <http://agda.github.io/agda-stdlib/Codata.Colist.html#1830> = <> a <http://agda.github.io/agda-stdlib/Codata.Colist.html#1853> ∷ <http://agda.github.io/agda-stdlib/Codata.Colist.html#1310> λ <> where <> . <>force <http://agda.github.io/agda-stdlib/Codata.Thunk.html#544> → <> [] <http://agda.github.io/agda-stdlib/Codata.Colist.html#1291>

 <>length <http://agda.github.io/agda-stdlib/Codata.Colist.html#1884> : <> Colist <http://agda.github.io/agda-stdlib/Codata.Colist.html#1245> A <http://agda.github.io/agda-stdlib/Codata.Colist.html#1187> i <http://agda.github.io/agda-stdlib/Codata.Colist.html#1174> → <> Conat <http://agda.github.io/agda-stdlib/Codata.Conat.html#527> i <http://agda.github.io/agda-stdlib/Codata.Colist.html#1174>
length <http://agda.github.io/agda-stdlib/Codata.Colist.html#1884> [] <http://agda.github.io/agda-stdlib/Codata.Colist.html#1291>       = <> zero <http://agda.github.io/agda-stdlib/Codata.Conat.html#558>
length <http://agda.github.io/agda-stdlib/Codata.Colist.html#1884> ( <>x <http://agda.github.io/agda-stdlib/Codata.Colist.html#1945> ∷ <http://agda.github.io/agda-stdlib/Codata.Colist.html#1310> xs <http://agda.github.io/agda-stdlib/Codata.Colist.html#1949>) <> = <> suc <http://agda.github.io/agda-stdlib/Codata.Conat.html#575> λ <> where <> . <>force <http://agda.github.io/agda-stdlib/Codata.Thunk.html#544> → <> length <http://agda.github.io/agda-stdlib/Codata.Colist.html#1884> ( <>xs <http://agda.github.io/agda-stdlib/Codata.Colist.html#1949> . <>force <http://agda.github.io/agda-stdlib/Codata.Thunk.html#544>) <>
The phrase “ <>λ <> where <> . <>force <http://agda.github.io/agda-stdlib/Codata.Thunk.html#544> → … <>” effectively plays the role of ‘freeze’ in conventional presentations of thunks while passing .force (e.g., “ <>xs <http://agda.github.io/agda-stdlib/Codata.Colist.html#1949> . <>force <http://agda.github.io/agda-stdlib/Codata.Thunk.html#544>”) is effectively ’thaw’. Is that right? <>

 <>
Thanks Again, <>
Bill <>

> On Apr 29, 2020, at 2:53 PM, Guillaume Allais <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 <http://agda.github.io/agda-stdlib/Codata.Colist.html>
> 
> And what you call transcript corresponds to our cowriter:
> http://agda.github.io/agda-stdlib/Codata.Cowriter.html <http://agda.github.io/agda-stdlib/Codata.Cowriter.html>
> 
> 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://lists.chalmers.se/mailman/listinfo/agda>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200503/f7d74c14/attachment.html>