Agda Implementors' Meeting XXX progress summary

Wednesday 11 September

• Jesper: working on the doublechecker.
• Ulf: started adding quoted terms to internal syntax. Currently doing boring boilerplate.
• Holger: looked at Jesper's summer school notes.
• Stephan: looked at Lambda-prolog.
• Gabor: get rid of codata keyword PR polished.
• Shaun and Martin: talked about Shaun's talk.
• Wen and James: proving easy lemmas about lifting alg. properties to vectors pointwise.
• Malin: getting uswed to the codebase.
• Evgenii: working on left hand side let.
• Guillaume: fixed a bug with irrefutable with.
• Nicolas with friends: converting Haskell code into Agda. Explored tools for logo competition voting. We vote on a draft, then we get a graphic designer to fix up the final logo.
• Fredrik: Catchall-clauses using reflection. Experimenting how far you can get without changing the reflection machinery.

Thursday 12 September

• Jesper: Demo of --cumulativity. Mostly working!
• Ulf: Demo of more efficient quotation. Quoting and unquoting is now fast; currently working on making it possible to inspect quoted terms again.
• Guillaume: Demo of implicit with expressions. Andreas says: please extend also to irrelevant with abstraction.
• Shaun: started writing a talk for Saturday.
• Fredrik: Finished show functions for reflection things.
• Andreas: worked on PR #854 to std-lib on disjoint unions of sublists.
• James and Wen: More linear algebra; defined a module of modules. Should the ring R be a field or a parameter?
• Nicolas: different ways of doing multiplication. Did some Agda proofs. Reviving the agda-parametricity library: would like to programmatically generate names using reflection. Ulf: can get quite far by using instance arguments and maintaining a lookup table.
• John: Playing with cubical Agda. Possibly found a bug with transport for vectors?

Friday 13 September

• Evgenii: working on turning pattern-matching lambdas that can be ordinary lambdas into such.
• Nicolas and the group: Exploring the new representation of binary numbers in the std-lib. Continued working on agda-parametricity library.
• John: Thinking about correct-by-construction second species counterpoint.
• Guillaume: Demo of internalising inspect pattern.
• Andreas: Demo of additions about All to the library.
• Shaun: half-way through the talk preparation.
• James and Wen: more linear algebra: addition, scaling of vectors, PR on R-modules about to go in. John: might be worth looking at UniMath to see how they've structured things.
• Malin and Holger: Two small low-hanging fruit things for the standard library.
• Jesper: --cumulativity in master. Demo of how category theory definitions become easier. Fewer than expected level annotations needed (no solver yet).
• Ulf: Demo on progress on quoted terms as literals. No difference in speed in Jesper's tactic library.
• Thorsten and Fredrik: discussed and started implementing in Agda how to represent the signature for inductive-inductive types.

Saturday 14 September

• Nicolas: Updating agda-parametricity library and an extension of the standard library. Demo of agda-parametricity. Remains to be done: update to deal with Agda's new implicit argument insertion strategy.
• Evgenii: turns out it is not so easy.
• Holger: the source code of Agda is starting to make sense. Started writing an experience document.
• Ulf: Almost everything is working (everything except compilation). Still looking for a performance improvement.
• Guillaume: All withs are now working. Still fighting with the parser.
• James and Wen: Demo of proposed additions to the standard library: vectors as Vec A n = Fin n -> A, and left and right modules. Relationship: vectors form modules. Next: matrix multiplication.
• Malin: Started on implementing default options in library files.
• Shaun: Talked with Thorsten (and vice versa) about universal QIITs/QW-types. Tried to construct dependent eliminators for QW-types.
• Jesper: Demo on two-level type theory. It's not obviously wrong. New sort SSet of strict sets. Short idea to implement cubical Agda using strict equality; face lattice is tricky.
• Fredrik and Thorsten: Continued to work on a new view of inductive-inductive types. Current representation too liberal, aiming for a more restricted representation.

Monday 16 September

• Guillaume: got the parser working yesterday, but not clear if it is clear. Instead, came up with a more general design together with Ulf today. Thorsten: would like to raise the request of smart case as an alternative to inspect.
• Martin: worked towards real numbers as signed digit streams. Potentially found a performance issue.
• Jakob: Arrived.
• Fredrik: talked with Jakob about his representation of inductive-inductive signatures, and Szumi-ficiation.
• James: argued with people on the Internet about his std-lib pull requests.
• Malin: can now add default options to library files, but nothing happens yet.
• Andreas: discussed copatterns and a possible syntax for quotient coinductive types with Thorsten.
• Ulf: Good news: there are use cases for quoted literals with improved performance. Bad news: bugs have been found.
• Jesper: people have started to use --cumulativity. Started to implement a simple version of a constraint solver in order to lift cumulativity through datatypes.
• John: played more with cubical.
• Wen: tried to things with cubical, planned a talk, planned the next AIM.

Tuesday 17 September

• Guillaume revised his sized IO repo.He implemented a stopwatch added bindings for directory operations.
• James: experimented with different ways to do decidability. Used a variant which uses a Sigma-type with Booleans (EDec). Representation of finite subsets of Fin.
• Wen: found out that she can use reflection without instance arguments for the book.
• Nils? : some proofs on polynomials, no use of reflection
• Jevgenij : hopes to finish transformation from extended lambdas to normal lambdas
• Andreas: demonstrates use of a BNFC agda backend. Goal is to write a C compiler in agda.
• Jakob: with Thorsten tried to prove correctness of part of the translation from IITs -> IFs
• Malin : works on adding pragmas to library files (e.g. safe, without-K).
• Holger: looks for a small task to solve to improve understanding.
• Jesper: 2 things: was working with ULF on the forcing optimisation, e.g. arguments that can be determined from the types don't need need to be stored (cf Edwin's work). also was working cumulatively. Sidetracked with refactoring representations of universe levels. Problem with cubical agda (relies on a bug). Missing Andrea :-(
• John: Musical counterpoint in agda. (based on work with Youyou Cong). Started to work on 2nd species. Well-typed music cannot sound wrong.
• Thorsten: would like to have constructor (flexible sequence of constructors) and destructor (having destructors which are not fields) for next AIM (unless somebody does it before.