# 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