Agda Implementors' Meeting XXVI progress summary

AutoZero:

• Monday: preparation work by reading papers (John)
• Tuesday: auto in Agda by Wouter Swierstra, found internal error in Agda, Jesper to blame (John)
• Tuesday: fixing the internal error triggered by John's investigations (Jesper)
• Wednesday: Fixed the internal error from yesterday; read some more of the Auto in Agda (John)
• Friday: finished reading paper, trying to debug current code (John, Jesper)
• Saturday: located error in depth-first search, compilation now working with 2.5.4 (John)

Introduction to Agda

• Monday: got some remarks, discussion (Peter, Fredi)
• Tuesday: continued working on lecture notes, got more remarks (Peter)
• Tuesday: open problem in type theory: print lambda in the LaTeX backend (Peter)
• Wednesday: Finished writing the material (Peter)
• Friday: updating 'Agda as a logical system', discussion about layout of document, Agda as a LF theory (Peter, John, Jesper, Ulf, Ambrus)
• Friday: continued solving Agda exercises (Fredi)

Reducing Inductive-Inductive to inductive

• Monday: discussion (András, Fred, Ambrus)

Dependent type providers

• Monday: discussion (Guillaume, Ulf)
• Wednesday: started the implementation (Guillaume, Fred)
• Friday: wrapper around GHC backend to generate Haskell code to have uniform interface to generated code (Guillaume, Fred)
• Saturday: compilation working. Next step: making functions available to reduction machinery. (Guillaume, Fred)

Fine-grained classification of warnings

• Monday: In process of implementation (Guillaume, Fred)
• Tuesday: finished, added pull request, fixed build (Guillaume, Fred)

GHC backend heap representation

• Monday: Detagging of pointers (Gábor)

Graph reduction

• Monday: working on code generation for abstract machine (Csaba)

Higher inductive types

• Monday: added ability to declare path constructors (Andrea)
• Monday: refactor constructors to take eliminations: (probably) working! (Andrea)
• Tuesday: pattern matching on HITs works, but no coherence check yet, fixed positivity checker to allow path constructors (Andrea)
• Wednesday: Eliminator for the torus, clean-up of yesterday's commits (Andrea)
• Friday: Implementation mostly done. (Andrea) Examples: Interval, Circle, Set/Prop truncation, Torus, CCC's Still TODO: composition
• Saturday: fixed bug found by Jesper (Andrea)

Inversion

• Monday: fix bug with looping constraint solver by having maximum number of inversions (Ulf)
• Monday: started working on actual improvements (Ulf)
• Tuesday: fixed bug, added inversion improvements, still space for more improvements (Ulf)
• Wednesday: finished the inversion sprint (Ulf)
  • stuck type-level function can also use inversion
  • support for partially invertible functions
• Friday: fixing bugs found by Nisse (Ulf)

Forced constructor patterns

• Monday: Finished implementation (Jesper)

Heap representation of lambda-calculus

• Tuesday: discussed call by need evaluation with heap representation of lambda-calculus (András, Andreas)
• Tuesday: prototype implementation (Andreas)
• Wednesday: Refactored and got bidirectional TT using the heap representation (Andreas)
• Friday: implemented a logical framework, call-by-need working (Andreas)
• Saturday: thinking about how to do free variable analysis, found unsound eta-contraction in Agda (Andreas)

Universe level omega

• Tuesday: there is a level omega now, no pull request yet (Jesper)
• Tuesday: implemented omega-in-omega, accidentally enabled type-in-type, type checking loops, needs more thinking, no pull request yet (Jesper)
• Wednesday: hitting a wall: would require a lot of incompatible changes (Jesper)

Postponing of LHS checking

• Wednesday: basic version, mostly working (cf. issues #2056, #2926) (Jesper)
• Friday: finished implementing (Jesper)

Faster C quicksort than stdlib

• Wednesday: with SIMD instructions (Stephan is happy)

Pasting schemes of omega-categories

• Friday: Agda implementation (András, Gábor)
• Saturday: using de Bruijn levels instead of indices (Gábor)

Type inference calculus

• Friday: implementation in Haskell, worked on presentation for tomorrow (Peti)
• Saturday: gave presentation (Peti)

Speeding up reduction

• Friday: Thinking about how to make it slow and then speed it up (Ulf)
• Saturday: implemented part 1 (making everything slower) (Ulf)
• Saturday: trying to fix performance of inverse scope lookup (Ulf)

Documentation of irrelevance

• Saturday: Port documentation from wiki & test suite (Jesper)
• Saturday: Proofreading (John)

Unproductive people

• Monday: don't remember (Andreas)
• Tuesday: Peti, mystery person, Ambrus, Gábor
• Wednesday: Ambrus, Peti
• Friday: Ambrus
• Saturday: Ambrus (again!), Fredi, Eric