Agda Implementors' Meeting XXXII

The thirty-second Agda Implementors' Meeting will take place between 2020-05-25 and 2020-06-05. Everyone who uses Agda is invited to attend.

Due to the current pandemic the meeting will be held online. It will be held over two weeks instead of one, but each day might be less intense than in previous meetings. We will try to accommodate participants from different time zones. Please indicate at what times of the day that you are available when registering.

(An aside related to numbering: AIM XXXI was postponed. It is planned to be held later, and has kept its number. Thus AIM XXXII might be held before AIM XXXI.)

Important dates

2020-05-10
Soft deadline for registration
2020-05-11 to 2020-05-15
People can express interest in code sprints
2020-05-25 to 2020-06-05 (weekdays only)
AIM XXXII

Registration

You register for the meeting by entering your name below. Registration is not compulsory. Please also enter proposals for talks, discussions and code sprints below.

Technology

It is likely that talks and discussions will be held via Zoom. Code sprints will be coordinated on the Agda meeting Slack, which can be joined here.

Programme

The following programme is preliminary. Links to Zoom (or something like that) will be added later. Note: UTC is used for dates and times.

  • Monday 2020-05-25:
    First session (Zoom):
    • 10-11: Introduction
    • 11-12: Discussion: Matthew Daggitt: Implementing refactoring tools for Agda
    Second session:
    • 15-16: Thorsten Altenkirch: The symmetry of cubism
    • 16-16:30: Wrap-up meeting
  • Tuesday 2020-05-26:
    • 13-14: Discussion: Jesper Cockx: Revising Agda's module system
  • Wednesday 2020-05-27:
    • 10-11: Discussion: Thorsten Altenkirch: Fixing cubical
    • 11-11:30: Wrap-up meeting
    • 15-16: Talk: Jesper Cockx: To infinity, and beyond! On the need for sorts bigger than Setω
  • Thursday 2020-05-28:
    • 12-13: Talk: John Leo: Music Tools
  • Friday 2020-05-29:
    • 10-11: Talk: Artem Shinkarov
    • 15-16: Talk: Arjen Rouvoet
    • 16-16:30: Wrap-up meeting
  • Monday 2020-06-01:
    • 12-13: Talk: Nils Anders Danielsson: Some tricks for making Agda code faster
    • 13-13:30: Wrap-up meeting
  • Tuesday 2020-06-02:
    • 15-16: Talk: Uma Zalakain: π with leftovers: a mechanisation in Agda
  • Wednesday 2020-06-03:
    • 12-13: Talk: Joris Ceulemans: Modal Type Theory in Agda Using Presheaves
    • 13-13:30: Wrap-up meeting
  • Thursday 2020-06-04:
    • 10-11: Talk: James Wood: Why does Dec look funny these days?
  • Friday 2020-06-05:
    • 12-14: Final wrap-up meeting

Registered participants

If you are not working during "normal business hours" you may want to give a time zone that differs from the one in effect at your physical location.

NameTime zone
Nils Anders DanielssonUTC+2
Jesper CockxUTC+2
John LeoUTC-7
Herminie PagelUTC+2
Jakob von RaumerUTC+2
Jacques CaretteUTC-4
Fredrik Nordvall ForsbergUTC+1
Víctor López JuanUTC+2
Andreas AbelUTC+2
Tesla Ice ZhangUTC+8
Jannis LimpergUTC+2
Matthew DaggittUTC+8 (probably available at ~ UTC+2)
Yotam DvirUTC+2
Ulf NorellUTC+2
Joris CeulemansUTC+2
Martin EscardoUTC+1
Brent YorgeyUTC-5
Liang-Ting ChenUTC+8
Roman KireevUTC-2
Ting-Gan LUAUTC+8
Orestis MelkonianUTC+1
Evgeny PoberezkinUTC+1
James WoodUTC+1
Tomas MöreUTC+2
Sandro StuckiUTC+2
Jason HuUTC-4
Andrea VezzosiUTC+2
Zeji LiUTC+1
Patrik JanssonUTC+2
Chao-Hong ChenUTC-4
Ana BoveUTC+2
Thierry CoquandUTC+2
Thorsten AltenkirchUTC+1
Stefania DamatoUTC+2
Peter DybjerUTC+2
Anton SetzerUTC+1
Reed MullanixUTC-8
Uma ZalakainUTC+1
Adam WynerUTC+1
Stephan AdelsbergerUTC+2
Arved FriedemannUTC+2
Nicolai KrausUTC+1
András KovácsUTC+2
Ambrus KaposiUTC+2
Wen KokkeUTC+1
Artem ShinkarovUTC+1
FavoniaUTC-5
Wolfram KahlUTC-4
Scott WalckUTC-4
Marko DimjaševićUTC+2
Mietek BakUTC+2

Talk proposals

List talk proposals here.

  • Jesper Cockx: To infinity, and beyond! On the need for sorts bigger than Setω
    Something about https://github.com/agda/agda/pull/4609
  • John Leo: Music Tools
    An update on the progress of tools written in Agda for the analysis and synthesis of music. Joint work with Youyou Cong.
  • Joris Ceulemans: Modal Type Theory in Agda Using Presheaves
    Presentation of work in progress on a shallow embedding of modal (dependent) type theories in Agda using presheaves.
  • Arjen Rouvoet: TBC
  • Artem Shinkarov: Extraction in Agda
    I would like to share my experience of creating an extractor for a shallowly-embedded DSL. The extractor is written in Agda using the Reflection library. The interesting points are: turning a patten-mathcing lambda into a function with a nested conditional; translating type invariants into assertions of the target language; using rewrite rules to "optimise" expresions prior the extraction. For the latter the tricky bit was to push normalisation under the branches of the pattern-matching lambda, which requires to compute the valid typing context for the chosen branch of the pattern-matching tree.
  • Uma Zalakain: π with leftovers: a mechanisation in Agda
    We use leftover typing on a set of partial commutative monoids to mechanise a π-calculus with shared, graded and linear channels.
  • James Wood: Why does Dec look funny these days?
    It used to be that the answer to a decision problem was either yes followed by a proof or no followed by a refutation. But now, using a recent version of the Standard Library, when you pattern match on a variable of type Dec P, you get does1 because proof1, leaving you little the wiser on what the result actually was. In this talk, I'll explain why this is a good (and sometimes crucial) thing, and what new best practices it entails for working with decision procedures.
  • Thorsten Altenkirch: The symmetry of cubism
    In old agda we could do inductive proofs by pattern matching and structural recursion. My observation is that in cubical agda we can do coinductive proofs by copattern matching and guarded recursion. My message is that cubical is good for more then proving univalence or performing higher dimensional homotopical proofs inaccessible to ordinary mortals.
  • Nils Anders Danielsson: Some tricks for making Agda code faster
    I plan to show some tricks I have used to make my Agda code type-check faster.
  • Name: Title
    Abstract

Discussion proposals

List discussion proposals here.

  • Jesper Cockx: Revising Agda's module system
    In the 13 years since the original release of Agda 2, the module system designed by Ulf Norell has proven itself to be powerful and robust for many applications. However, two pain points in the current implementation are the printing of names coming from imported modules, and the efficiency issues (e.g. https://github.com/agda/agda/issues/4331) arising from the need to copy modules on application. This would be a good time to revisit the original design and see what can be improved with our current knowledge.
  • Matthew Daggitt: Implementing refactoring tools for Agda
    There are now some relatively large Agda code bases floating about (the standard library itself is now over 80kloc) and consequently the lack of a smarter editing environment for Agda is becoming more of an issue. Tools that would be useful include refactoring support, automatic import suggestions, and redundant import analysis. It would be great if the relevant parts of the community could share their experience on prior attempts to implement similar tools and on what they see as the best way forward is. Tentative suggestions might include extending Emacs mode and/or Atom mode with additional functionality, or implementing the Language Server Protocol and using the functionality in existing editors such as Eclipse.
  • Thorsten Altenkirch: Fixing cubical
    There are some things to do do make cubical working in practice. I hope we can roll out Andrea's implementation of inductive families (this needs some testing). We should integrate Jesper's implementation of a 2-level type theory into the cubical theory (e.g. I should live there) and library. We need some discussion how cubical should look like in the future. This may feed into a code sprint.
  • Stephan Adelsberger and Anton Setzer: Optimising Agda
    1. Equality check possible which allows to check 10^(10^10) = 10^(10^10 + 0) in a millisecond using techniques from automated theorem proving
    2. Brute force guess proofs with parallel cluster
    In principle, most Agda code written can be type-checked by hand, but if one type checks in Agda often very powerful machines are needed. One reason is that equality is checked by reducing terms to normal form. For instance 10^(10^10) = 10^(10^10 +0) is no longer checkable in (our version of) Agda, whereas by hand one can easily verify it. The question is whether one could write efficient equality checkers which do what a human person would do.
    Another problem we observed was when defining a function f : (a : A) -> (b : B a) -> (c : C a b ) -> bottom where A, B a C a b are finite sets and in all cases one of them is empty. In Agda, this had to be done manually, and it took a very long time even after the case distinction had been manually carried out. There are two aspects: one is that the case distinction should be done automatically and the other is that type checking cannot be done in a parallel way. In the latter case, each finite subcase could be represented as a separate Agda file and sent to a cluster of machines. Then, each machine runs Agda and the one machine that finds the empty case reports back.
  • Stephan Adelsberger and Anton Setzer: Combining Agda with external tools
    1. Interface which allows to add external tools (e.g. SAT solvers, model checkers, other decision procedures) to Agda, integrating work by Karim Kanso.
    2. Integration of Lambda prolog with Agda
    3. SPARK Ada with Agda why3
    We discuss various ways of combining Agda with external tools. One is to reactivate the work by Karim Kanso for an older version of Agda, where he allowed to write flexible builtins. He used it to integrate a SAT solver and a model checker with Agda to verify real world railway interlocking system. Another tool to consider is to interface the why3 system with Agda. The why3 system allows to create from ML style programs with Hoare-logic style verification conditions (pre-conditions, post conditions, intermediate check conditions) verification conditions which are then solved by various automated and interactive theorem prover, including Coq. The SPARK system for writing critical system uses the why3 system to verify code written in it. Using an Agda interface for why3 programs written in SPARK could be verified in Agda. The third external tool we want to consider is lambda prolog.
  • Proposer: Title
    Explanation.

Code sprint proposals

List code sprint proposals here.

  • Matthew Daggitt: Tactics in the Standard Library
    The Standard Library has recently added its first tactics using Agda's reflection framework, and is currently looking for more. This code sprint would firstly be an opportunity for anyone who has developed useful tactics or tactic-related utilities to contribute them to the library. Secondly, those who have some experience developing tactics might be available to provide some pointers to those (such as myself) who are just starting out.
    People who are interested in taking part in the code sprint: Matthew Daggitt, Jesper Cockx, Tomas Möre, Reed Mullanix, Nils Anders Danielsson.
  • James Wood: Typed pattern synonyms
    Agda's pattern synonyms, introduced by the pattern keyword, are currently untyped. While this is a simple and lightweight solution, it causes several problems:
    1. Normal constructors can be overloaded based on their type. This is very useful when working with two similarly structured types at the same time, like List and All. But pattern synonyms have no type, so cannot be overloaded like this.
    2. When a pattern can be rewritten using a pattern synonym, Agsy tends to do this eagerly. Often this happens as a coincidence, perhaps due to overloading of constructors, producing a confusing and morally ill typed result.
    3. There is no sanity checking of pattern synonyms. Pattern synonyms may have a definition that is ill formed, and there is no warning of this.
    4. There is no interactive editing support when writing a pattern synonym. Standard practice is to define a function of the desired type, then delete the type and add the word pattern.
    5. Pattern synonyms are not self-documenting, because we had to delete the type declaration.
    6. Pattern synonyms cannot handle implicit arguments well. With types, it would make sense to solve implicit arguments like normal for constructors and functions.
    I propose that we implement typed pattern synonyms to alleviate some of these problems, and to have a chance of alleviating them all eventually.
    Relevant issue: #2069
    People who are interested in taking part in the code sprint: James Wood.
  • Thorsten Altenkirch : An Agda REPL integrated in emacs
    When teaching with agda I miss an agda top level where I can evaluate expressions interactively. C-c C-n doesn't really cut the ice! Hence I would like to resurrect interactive agda and integrate it into the emacs mode (maybe also for other editors). That is I would like to press some keys and the current buffer is loaded into interactive agda which shows up in a different buffer.
    I need somebody who knows emacs lisp and maybe has some experience with the agda mode.
  • Thorsten Altenkirch: Destructors for indexed records and coinductive types
    I would like to be able to write:
   record Vec (A : Set) : ℕ → Set where
     coinductive
     destructor
       hd : {n : ℕ} → Vec A (suc n) → A
       tl : {n : ℕ} → Vec A (suc n) → Vec A n
see issue 4650 for an explanation.
  • Anton Setzer: A Mechanism for the flexible addition of external tools to Agda
    In his PhD thesis Karim Kanso created a mechanism in Agda for flexibly adding builtins to Agda. This was used integrate a SAT solver and a model checkers into Agda by overriding an existing but inefficient decision procedure in Agda by an external tool. Such a mechanism would allow in general to add external tools at type checking to Agda. Karim used this in order to verify a real world railway interlocking system in Agda. He proved specific properties of the concrete interlocking systems using the external tools and carried out more generic proofs in standard Agda. Karim created a fork of Agda which has never integrated into main Agda, and this fork would need to be updated.
    I'm myself an experienced user but not an implementer of Agda and would need some help with this. Because of my schedule week 2 would be more suitable for this project but I would of course support those wanting to start with this project earlier.
    Karim Kanso wrote when contacted : "The good news is that it does not appear to have diverged too much. All the needed insertion points remain and look very similar, however, inevitably some of the function names, types and modules have changed. This is where the effort needs to be spent."
    Karim, who has not been working with Agda or Haskell for some time, wrote as well that he would be happy to attend for a focused session, such as a discussion related to external tools to provide any input.
    There is a git repository with the Agda fork of Karim, the PhD thesis by Karim can be found here, and here you can find a publication by Karim and myself about this project.
Page last modified on May 24, 2020, at 09:36 PM
Powered by PmWiki