[Agda] list comprehensions

[James Wood]

Dear Sergei,

List comprehensions are very similar to do notation, which Agda already
supports. See:


https://agda.readthedocs.io/en/v2.6.0.1/language/syntactic-sugar.html#do-notation

Your example would then look like the following.

  do
    ((i , p) , j) ← items
    return ((i , j) , p)

However, note that if you have to make proofs about this expression,
it's likely that it's going to be slightly more difficult to work with
than the version using `map`. The do notation desugars and computes to

  concat (map (λ i → f i ∷ []) items)

where f is the function that rearranges the tuple. In other words, we
are concatenating lots of one-item lists, rather than just having a list.

With this in mind, you might want to keep the `map` version, but do some
things to make it nicer. The most direct is the `λ where` syntax, that
allows pattern matching.

  map (λ where ((i , p) , j) → ((i , j) , p)) items

This can cause issues when you want to repeat this expression somewhere
else, in which case you can rewrite to something more verbose.

  map (λ item → let ((i , p) , j) = item in ((i , j) , p)) items

I believe in the development version of Agda, it's even possible to
write the following.

  map (λ ((i , p) , j) → ((i , j) , p)) items

This will behave identically to the `let` version.

Regards,

James

On 10/12/2019 20:04, mechvel at scico.botik.ru wrote:
> Dear Agda developers,
> 
> list comprehensions is a nice feature in Haskell.
> For example, I write
>     [((i, j), p) | ((i, p), j) <- items]
> 
> to transform a list of "triples".
> But in Agda, one has to write
>     map (\item → ((proj₁ $ proj₁ item , proj₂ item) ,
>                   (proj₂ $ proj₁ item)
>                  )
>         ) items
> 
> This code is difficult to perceive.
> Well, I do not know how of difficult can it be to introduce list
> comprehensions to Agda
> (to language? to library?).
> 
> Regards,
> 
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda