[Agda] Lists and products

Fri Mar 2 13:07:20 CET 2018

Guillaume,

Thank you for the suggestion. I tried something similar, but gave it up
because I wanted to write

  map (1 +_) [ 0 , 1 , 2 ]

rather than

  map (1 +_) ([ 0 , 1 , 2 ])

in examples. Thank you for the point about 'pattern', which should apply to
either method. Thank you also for the example of using `_` to name an
example, which I had not seen before and is much more convenient than using
ex1, ex2, ..., which may need to be renamed if other examples are added in
the middle.

Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On 2 March 2018 at 12:51, Guillaume Allais <guillaume.allais at ens-lyon.org>
wrote:

> Hi Phil, instead of declaring all of these toplevel definitions
> with different arities, you can use infix identifiers. Even better:
> using pattern-synonyms you'll be able to use these on the left
> hand side!
>
> =================================================
> module poc.list-literals where
>
> open import Agda.Builtin.List
>
> module _ {ℓ} {A : Set ℓ} where
>
>   infix 1 [_
>   infixr 2 _,_
>   infix 3 _]
>
>   -- [_ : List A → List A
>   pattern [_ xs = xs
>
>   -- _,_ : A → List A → List A
>   pattern _,_ a as = a ∷ as
>
>   --  _] : A → List A
>   pattern _] x = x ∷ []
>
>
> open import Agda.Builtin.Nat
>
> _ : List Nat
> _ = [ 1 , 2 , 3 , 4 ]
>
> open import Data.Maybe
>
> last : List Nat → Maybe Nat
> last ([ x ])  = just x
> last (x ∷ xs) = last xs
> last _ = nothing
> =================================================
>
> On 02/03/18 12:40, Philip Wadler wrote:
>
> And now a simpler question.
>
> In order to make it handy to write examples with lists, it is handy to
> define:
>
> [_] <https://wenkokke.github.io/Lists#2988> : ∀ {A <https://wenkokke.github.io/Lists#2997> : Set} → A <https://wenkokke.github.io/Lists#2997> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#2997>[ <https://wenkokke.github.io/Lists#2988> z <https://wenkokke.github.io/Lists#3021> ] <https://wenkokke.github.io/Lists#2988> = z <https://wenkokke.github.io/Lists#3021> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
> [_,_] <https://wenkokke.github.io/Lists#3035> : ∀ {A <https://wenkokke.github.io/Lists#3046> : Set} → A <https://wenkokke.github.io/Lists#3046> → A <https://wenkokke.github.io/Lists#3046> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#3046>[ <https://wenkokke.github.io/Lists#3035> y <https://wenkokke.github.io/Lists#3074> , <https://wenkokke.github.io/Lists#3035> z <https://wenkokke.github.io/Lists#3078> ] <https://wenkokke.github.io/Lists#3035> = y <https://wenkokke.github.io/Lists#3074> ∷ <https://wenkokke.github.io/Lists#856> z <https://wenkokke.github.io/Lists#3078> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
> [_,_,_] <https://wenkokke.github.io/Lists#3096> : ∀ {A <https://wenkokke.github.io/Lists#3109> : Set} → A <https://wenkokke.github.io/Lists#3109> → A <https://wenkokke.github.io/Lists#3109> → A <https://wenkokke.github.io/Lists#3109> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#3109>[ <https://wenkokke.github.io/Lists#3096> x <https://wenkokke.github.io/Lists#3141> , <https://wenkokke.github.io/Lists#3096> y <https://wenkokke.github.io/Lists#3145> , <https://wenkokke.github.io/Lists#3096> z <https://wenkokke.github.io/Lists#3149> ] <https://wenkokke.github.io/Lists#3096> = x <https://wenkokke.github.io/Lists#3141> ∷ <https://wenkokke.github.io/Lists#856> y <https://wenkokke.github.io/Lists#3145> ∷ <https://wenkokke.github.io/Lists#856> z <https://wenkokke.github.io/Lists#3149> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
> [_,_,_,_] <https://wenkokke.github.io/Lists#3171> : ∀ {A <https://wenkokke.github.io/Lists#3186> : Set} → A <https://wenkokke.github.io/Lists#3186> → A <https://wenkokke.github.io/Lists#3186> → A <https://wenkokke.github.io/Lists#3186> → A <https://wenkokke.github.io/Lists#3186> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#3186>[ <https://wenkokke.github.io/Lists#3171> w <https://wenkokke.github.io/Lists#3222> , <https://wenkokke.github.io/Lists#3171> x <https://wenkokke.github.io/Lists#3226> , <https://wenkokke.github.io/Lists#3171> y <https://wenkokke.github.io/Lists#3230> , <https://wenkokke.github.io/Lists#3171> z <https://wenkokke.github.io/Lists#3234> ] <https://wenkokke.github.io/Lists#3171> = w <https://wenkokke.github.io/Lists#3222> ∷ <https://wenkokke.github.io/Lists#856> x <https://wenkokke.github.io/Lists#3226> ∷ <https://wenkokke.github.io/Lists#856> y <https://wenkokke.github.io/Lists#3230> ∷ <https://wenkokke.github.io/Lists#856> z <https://wenkokke.github.io/Lists#3234> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
> [_,_,_,_,_] <https://wenkokke.github.io/Lists#3260> : ∀ {A <https://wenkokke.github.io/Lists#3277> : Set} → A <https://wenkokke.github.io/Lists#3277> → A <https://wenkokke.github.io/Lists#3277> → A <https://wenkokke.github.io/Lists#3277> → A <https://wenkokke.github.io/Lists#3277> → A <https://wenkokke.github.io/Lists#3277> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#3277>[ <https://wenkokke.github.io/Lists#3260> v <https://wenkokke.github.io/Lists#3317> , <https://wenkokke.github.io/Lists#3260> w <https://wenkokke.github.io/Lists#3321> , <https://wenkokke.github.io/Lists#3260> x <https://wenkokke.github.io/Lists#3325> , <https://wenkokke.github.io/Lists#3260> y <https://wenkokke.github.io/Lists#3329> , <https://wenkokke.github.io/Lists#3260> z <https://wenkokke.github.io/Lists#3333> ] <https://wenkokke.github.io/Lists#3260> = v <https://wenkokke.github.io/Lists#3317> ∷ <https://wenkokke.github.io/Lists#856> w <https://wenkokke.github.io/Lists#3321> ∷ <https://wenkokke.github.io/Lists#856> x <https://wenkokke.github.io/Lists#3325> ∷ <https://wenkokke.github.io/Lists#856> y <https://wenkokke.github.io/Lists#3329> ∷ <https://wenkokke.github.io/Lists#856> z <https://wenkokke.github.io/Lists#3333> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
> [_,_,_,_,_,_] <https://wenkokke.github.io/Lists#3363> : ∀ {A <https://wenkokke.github.io/Lists#3382> : Set} → A <https://wenkokke.github.io/Lists#3382> → A <https://wenkokke.github.io/Lists#3382> → A <https://wenkokke.github.io/Lists#3382> → A <https://wenkokke.github.io/Lists#3382> → A <https://wenkokke.github.io/Lists#3382> → A <https://wenkokke.github.io/Lists#3382> → List <https://wenkokke.github.io/Lists#813> A <https://wenkokke.github.io/Lists#3382>[ <https://wenkokke.github.io/Lists#3363> u <https://wenkokke.github.io/Lists#3426> , <https://wenkokke.github.io/Lists#3363> v <https://wenkokke.github.io/Lists#3430> , <https://wenkokke.github.io/Lists#3363> w <https://wenkokke.github.io/Lists#3434> , <https://wenkokke.github.io/Lists#3363> x <https://wenkokke.github.io/Lists#3438> , <https://wenkokke.github.io/Lists#3363> y <https://wenkokke.github.io/Lists#3442> , <https://wenkokke.github.io/Lists#3363> z <https://wenkokke.github.io/Lists#3446> ] <https://wenkokke.github.io/Lists#3363> = u <https://wenkokke.github.io/Lists#3426> ∷ <https://wenkokke.github.io/Lists#856> v <https://wenkokke.github.io/Lists#3430> ∷ <https://wenkokke.github.io/Lists#856> w <https://wenkokke.github.io/Lists#3434> ∷ <https://wenkokke.github.io/Lists#856> x <https://wenkokke.github.io/Lists#3438> ∷ <https://wenkokke.github.io/Lists#856> y <https://wenkokke.github.io/Lists#3442> ∷ <https://wenkokke.github.io/Lists#856> z <https://wenkokke.github.io/Lists#3446> ∷ <https://wenkokke.github.io/Lists#856> [] <https://wenkokke.github.io/Lists#842>
>
> This conflicts (in terms of parsing) with the standard notation for
> products, so I have altered that slightly:
>
> open import Data.Product <https://agda.github.io/agda-stdlib/Data.Product.html> using (_×_ <https://agda.github.io/agda-stdlib/Data.Product.html#1329>) renaming (_,_ <https://agda.github.io/agda-stdlib/Data.Product.html#543> to ⟨_,_⟩ <https://agda.github.io/agda-stdlib/Data.Product.html#543>)
>
> The question is, have I chosen the best way to deal with the situation? Or
> is there an alternative that others recommend? Cheers, -- P
>
>
> .   \ Philip Wadler, Professor of Theoretical Computer Science,
> .   /\ School of Informatics, University of Edinburgh
> .  /  \ and Senior Research Fellow, IOHK
> . http://homepages.inf.ed.ac.uk/wadler/
>
>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
>
>
> _______________________________________________
> Agda mailing listAgda at lists.chalmers.sehttps://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/20180302/a94ac136/attachment-0001.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180302/a94ac136/attachment-0001.ksh>