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

[Eric Finster]

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> 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> 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
>
> And what you call transcript corresponds to our cowriter:
> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200429/5cfb7fd2/attachment.html>