Agda Implementors' Meeting XXXIII Wrapup meetings

2020-10-13

Cubical:

• Anders: making library typecheck faster
• Andrea: exposing problem with incompatability between positivity checker and cubical

Release 2.6.1.2

• Andreas: backported 3 packages to support Stackage

More control over reduction:

• Jesper & co: added new primitives `onlyReduceDefs` and `dontReduceDefs`, needs more testing
• Artem: testing out new primitives, working great so far

2020-10-14

Quasiquoting:

• Ulf: Started to think about what we can write in current Agda. Demo with `!` operator for antiquotation. Magic weakening for variables. Does not work yet on the LHS.

Integrating erasure with univalence:

• Andrea: currently all types are checked in erased context, but this is unsound with univalence. Found bug with erasure (independent of univalence), see #4986.

Instances in stdlib:

• Jesper: proposed list of possible instances that could be added

Cubical:

• John: Fixed inconsistent terminology in cubical library (section and retraction). After discussion with Anders, replaced sec and ret in HalfAdjoint.agda with linv and rinv to be consistent with Isomorphism.agda. Note that this may break code depending on isHAEquiv.

Nix infrastructure:

• James: trying to update manual, discovering new things about nix

2020-10-16

Jesper: working on issue #4727

Ulf: using instance arguments to ensure absense of antiquotes outside of any quote.

Andrea: fixed two bugs with erasure

2020-10-19

Sized types:

• Andreas: We had discussion on sized types, try to find solution for current inconsistencies by getting closer to theory from ICFP 2013 paper.
• Jesper: trying to find the cause of #4995 (see analysis on github)

2020-10-22

Producing readable Haskell

• Ulf, James, Jesper: First prototype of Agda2Hs backend to compile Agda to readable Haskell code (see https://github.com/agda/agda2hs).

Sized types:

• Andreas, Manuel: Had another discussion, outcome unclear (?)

Inductive families in cubical

• Andrea: trying to make termination checker accept more definitions --without-K, fixing #4527.

Quasiquoting:

• Ulf: Enforcing well-formedness of quasiquotes using InsideQuote` tactic argument, now works --safe.

Artem: Working on fixing the `reconstructParameters` function and exposing it to reflection API

2020-10-23

Reflection:

• Ulf: made some PR for annotated reflected syntax (usable by Schmitty the Solver)
• Wen & Thomas: looking at CVC proof rules for Schmitty

Cubical:

• Andrea: working on indexed families
• Anders: merged a bunch of PRs, made draft of naming convention

Agda2hs backend:

• Ulf: generating haskellSrcExt instead of plain strings
• Ulf: added support for lambdas
• James: extending the backend with support for type classes

Sized types:

• Andrea: Still not clear if there's a design that guarantees consistency + subject reduction. There should be a paper to study combination of sized + dependent types. Maybe we can take inspiration from "Practical sized types for Coq" paper?
• Andreas: re-activated SizeUniv

Quasiquoting:

• Ulf: Another demo of the same thing as yesterday

Improving of support for erasure:

• Nisse, Andrea: fixed issue with erased parameters of data/record types
• Nisse: identified problem with compiling functions with erased identifiers in their type

Clause telescopes in reflected syntax (code sprint from previous meeting):

• Jesper: implemented checking of types in the telescope when unquoting a clause

Interleaving constructors and clauses

• Guillaume: made a PR https://github.com/agda/agda/pull/5001, desugars to new-style mutual blocks