Agda Implementors' Meeting XXIII progress summary

Wednesday 20 April

  • Jesper: Found bug when using rewriting, plan to fix it.
  • Ulf, Nisse, Guillaume, Andreas, Victor, Shayan: talked about do-notation, layout and copatterns. Decided that "lambda where" is good notation for a layout-aware pattern-matching lambda.
  • Conor, Andreas, many others: Discussed cumulativity. Will experiment with using universe constraints instead of lsuc, lmax.
  • Ulf: pushed idiom-brackets.

Thursday 21 April

  • Ulf: flexible module parameters
  • Andreas: Overloaded record fields
  • Jesper: Higher Order REWRITING
  • James, Fred, Guillaume: Typechecking despite termination check failure
  • Henning: Adding codata, bisimulation and up-to techniques to the standard library

Friday 22 April

  • Ulf: fixing bugs related to flexible module parameters
  • Nisse: Module names are hashed, turns out the hashing function is not injective (exploit)
  • Andrea: Experiments towards Cubical TT in Agda using BUILTINs and PRIMITIVEs
  • Jesper: Experiments towards Cubical TT in Agda using REWRITE rules
  • Andreas: Considerations on the ordinal iterations necessary to take the fixpoint of a strictly-positive indexed family
  • Guillaume, Fred: Further work on non-fatal errors.

Saturday 23 April

  • Andreas: Copattern matching with overloaded projections now also works (issue 1944)
  • Conor: a formal language for multi-sorted syntaxes with binding and their typing rules
  • Jesper: a logo for Agda
  • Fred, Guillaume: Displaying aggregated errors in the emacs buffer.
  • Henning: Structure of the standard library regarding Codata

Monday 25 April

  • Andrea: Cubical-in-Agda: J now computes. Cannot yet do coercion, or handle inductive families. Time for equality-agnostic inductive families?
  • Ulf: Closer to a working implementation of flexible module parameters. 40 39 30 24 failing test cases to go.
  • Bob: Demo of Foveran, a language with a universe of descriptions of data types.
  • Victor: Support for more literate code formats:
    • split up literate code support from lexer
    • added support for the rst format
    • mostly works, but some highlighting problems with identifiers
  • Victor: some logo suggestions
  • Jesper: fixed another REWRITE bug related to interaction with the constraint solver.
  • Nisse: an optimisation.
  • Andreas: Still working on overloaded projections; a few things cannot be fixed due to lack of postfix projection syntax, so maybe introduce that as well?
  • Guillaume, Fred: started refactoring warnings.
  • Edwin: looked at Nisse's challenge in Idris.

Tuesday 26 April

  • Jesper: documentation code-sprint on indexed data types, strict positivity, pattern-matching (including dot and absurd patterns)
  • James: Normalisation by Evaluation in the Delay monad: proving termination, soundness and completeness independently