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