Agda Implementors' Meeting XXXIV

The thirty-fourth Agda Implementors' Meeting will take place between 2021-06-07 and 2020-06-12. Everyone who uses Agda is invited to attend.

Due to the current pandemic the meeting will be held online. We will try to accommodate participants from different time zones. Please indicate at what times of the day that you are available when registering.

Important dates

2021-05-31

Soft deadline for registration

2021-06-01 to 2021-06-06

People can express interest in code sprints

2021-06-07 to 2021-06-12

AIM XXXIV

Registration

You register for the meeting by entering your name below. Registration is not compulsory. If you would like to give a talk or propose a discussion or code sprint, please add this to the list below.

Links and Technology

All talks and discussions can be attended through Zoom (same link for all talks) if you want to participate in the discussion or via Twitch if you're happy to just listen in. Talks will be archived on Twitch for 14 days.

Similarly to the previous online Agda meeting, all code sprints and other text-based communication will be held via Zulip, which can be joined here. Don't forget to also join the aim-xxxiv stream which will contain all the information related to the meeting! To join Zulip from an app see the Zulip website.

Programme

Note: UTC is used for dates and times.

One hour has been scheduled for talks and discussions. However, note that it is fine to give a shorter talk, and discussions might take more than one hour if there is a lot of interest in them.

Monday 2021-06-07

• 09-12 UTC (11-14 CEST): Welcome + Planning of discussions and code sprints (asynchronously via Zulip)
• 12-13 UTC (14-15 CEST): Introductions
• 13-14 UTC (15-16 CEST): Talk by Edwin Brady: "Experiences with Implementing Idris 2 (not final title)"

Tuesday 2021-06-08

• 14-15 UTC (16-17 CEST): Talk by András Kovács: "Enhanced Pattern Unification"
• 15-16 UTC (17-18 CEST): Wrap-up meeting

Wednesday 2021-06-09

• 14-15 UTC (16-17 CEST): Talk by Jesper Cockx: "Verifying Five Haskell Libraries with Agda2Hs"
• 15-16 UTC (17-18 CEST): Wrap-up meeting

Thursday 2021-06-10

• 13-14 UTC (15-16 CEST): Talk by Robert Atkey: "Real Numbers in Agda" (as part of MSP101)
• 14-15 UTC (16-17 CEST): Talk by Lucas Escot: "Datatype-generic programming in Agda"
• 15-16 UTC (17-18 CEST): Wrap-up meeting

Friday 2021-06-11

• 13:30 UTC (15:30-16 CEST): Talk by Anton Setzer: "Decidable properties in Agda"
• 14-14:30 UTC (16-16:30 CEST): Talk by Nils Anders Danielsson: "--erased-cubical"
• 14:30-15:30 UTC (16:30-17:30 CEST): Wrap-up meeting
• 15:30- UTC (17:30- CEST): The Agda pub

Saturday 2021-06-12

Virtual excursion

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.

Talk and discussion proposals

• Edwin Brady: Experiences with Implementing Idris 2
• Jesper Cockx: Verifying Five Haskell Libraries with Agda2Hs
  Agda2Hs (https://github.com/agda/agda2hs) is a new backend for Agda that translates a subset of Agda to readable Haskell code. The main goal of this project is to write and verify code in Agda that can be integrated seamlessly into Haskell projects. In this talk I will report on the work done by five undergraduate students at TU Delft to port five Haskell libraries (Data.Map and Data.Sequence from the containers package, Data.Graph.Inductive from the fgl package, and the QuadTree and Ranged-sets packages) to Agda, verify their pre- and post-conditions and internal invariants, and translate the verified implementations back to Haskell using Agda2Hs.
• András Kovács: Enhanced Pattern Unification
  Pattern unification has been a core inference feature in dependently typed languages for a long time. Agda implements several extensions on the top of the basic algorithm. I propose a new extended pattern unification algorithm, which is quite efficient and finds more solutions than existing implementations. For example, if we have a bound variable "f", the algorithm can solve "?0 (\x y -> f y x) = f" as "?0 := \f x y -> f y x". I conjecture that the algorithm can invert meta spines modulo all definitional isomorphisms which are definable in a type theory with pi and sigma.
• Robert Atkey: Real Numbers in Agda (as part of MSP101)
  In a constructive logic real numbers are even more interesting than they are in the classical world. To demonstrate the differences, I'll talk about how we can construct a type of real numbers in Agda in terms of the Cauchy completion of the metric space of rational numbers. This yields an implementation of real numbers that is reasonably efficient and that we can do proofs about. The basic construction closely follows Russell O'Connor's "A monadic, functional implementation of real numbers". I'll also talk about using the completion of a metric space to implement quantitative equational theories over complete separable metric spaces in Agda. I'll try to work from the assumption that the audience knows nothing about metric spaces, completion, or construction of real numbers.
• Lucas Escot: Datatype-generic programming in Agda
  In languages like Haskell or Ocaml, where programmers are encouraged to introduced new datatypes at will to suit the problem at hand, some machinery is made available in the language itself to relieve users of the burden of reimplementing basic constructions again and again. With such a deriving mechanism, users can retrieve things like decidable equality for free. In Agda however, such a practical system is not available as is. Reflection is powerful and can get you quite far, but it's complex, tedious, and uses an untyped representation of terms. In this talk I will showcase a WIP library based on existing work, which provides an encoding of datatype descriptions and generic constructions (induction principle, printing, decidable equality) implemented in a type-safe way --- without reflection --- supporting a broad range of concrete Agda datatypes.
• Nils Anders Danielsson: --erased-cubical
  I will present the new and currently experimental flag --erased-cubical, which allows you to compile Cubical Agda code, given that (roughly speaking) glue is only used in erased settings, and higher constructors are erased.
• Thorsten Altenkirch : How to make cubical agda more usable?
  Recently, Ambrus and myself tried to use cubical Agda to formalize some HIITs (actually coherent type theory) but we ran into a number of issues when using hcomp or transp in constructors. Luckily Andrea and Evan suggested some workarounds which means that we can avoid this situation. However, I am wondering wether there is a more principled solution. This is a request for a discussion with some of the experts ob cubism.
• Anton Setzer: Decidable properties in Agda (Jww with Fahad F. Alhabardi)
  The standard library doesn't provide directly decisions procedures for decidable properties such as relations between natural numbers, but instead provides elements of Dec A, which provide not only the decision but as well a proof object for the relation in question. If one uses Dec A, then one gets a dependency on a proof which causes problems with intensional equality. The type Dec A was initially defined as an algebraic data type but was then changed to a record type. This looks at first hand as an unnecessary containerification of algebraic data types, but turns out to provide a separation between a decision and the proof. When looking at the standard library one rarely finds functions defined by case disctinction on decidable objects without using the proof object. The reason is that the proof object is needed in order to obtain termination and overcome partiality problems, resulting in functions depending on proof objects. It seems that a better separation between computational meaningful parts and proof objects is needed, and we discuss how proof irrelevance might avoid this problem.

Code sprint proposals

• Jesper Cockx: User-defined extensionality rules
  You know user-defined rewrite rules, but have you heard about user-defined extensionality rules? Andromeda has them, so Agda should get them too! Here's the background reading: https://arxiv.org/abs/2103.07397v1
  People who are interested in taking part in the code sprint: Jesper, John, ...
• Jesper Cockx: A Chez Scheme backend for Agda
  It seems Idris 2 is using Chez Scheme as a backend language to great effect. Would it be faster to target Chez Scheme instead of the existing GHC backend? There's only one way to find out!
  People who are interested in taking part in the code sprint: Jesper, Wen, ...
• James Wood: Reflection of modules
  It would be nice if macros could take in and generate modules. For example, bulk renaming macros could help us avoid code like this, that adapts isCommutativeMonoid to +-isCommutativeMonoid. Usage of a bulk renaming macro rename may look something like unquoteModule +-CommutativeMonoid = rename ("+-" ++_) (quoteModule (CommutativeMonoid monoid)). Issue: #5399.
  People who are interested in taking part in the code sprint: James Wood, Jacques Carette, Artem Shinkarov, ...
• John Leo: Integration of MusicTools and MuseScore
  MusicTools (https://github.com/halfaya/MusicTools) is an Agda toolkit for analysis and synthesis of music, and MuseScore is open source notation software. I would like to integrate the two so that, for example, one could select a passage of music in MuseScore, send that to MusicTools for analysis, and annotate the score with the result. MuseScore allows writing plugins using QML which can in turn call an external program, so most of the work should involve defining an appropriate data interchange format.
  People who are interested in taking part in the code sprint: John Leo, Orestis, ...
• James Chapman: upwards and onwards with agda2hs
  agda2hs is a backend for agda that aims to produce readable Haskell code. It started at the last AIM with great work from Ulf and Orestis. We are using it at IOHK to verify a few properties of a lambda term generator (originally written by Wen Kokke) that are hard to test but easy to prove. Jesper is giving a talk about using agda2hs for student projects which sounds very interesting! I would like to gather feedback on agda2hs so far, work on the next steps and consider whether it's a good time to make a (pre-) release.
  People who are interested in taking part in the code sprint: James, Jesper, Ulf, Orestis, ...
• Jean-Frédéric Etienne: Extending Agda with Model-Checking Algorithms
  This proposition is to integrate model-checking algorithms like BMC and K-Induction in Agda to facilitate the detection of counterexamples and invariant satisfaction for finite/infinite state-transitions systems. The objective is to invoke external SAT/SMT solvers via specific tactics to perform automatic verification. Such tactics would be defined with a specific instance argument specifying the characteristics expected by a state-transition system to be verified. The integration of the backend solvers must be performed in such a manner so as to facilitate incremental SMT solving. Indeed, symbolic bounded model-checking requires an unrolling step that is performed at each analysis depth (i.e., each SMT query). Incremental SMT solving is essential in this case as the solver instance may use learned clauses/facts from previous queries to resolve the current one. For invariant satisfaction tactics, it may also be interesting to add a proof reconstruction feature to cross-check the resolution tree produced by the SAT/SMT solver for each "valid" query. The work currently being carried out within the scope of the Schmitty project (https://github.com/wenkokke/schmitty) seems to be a good candidate for this proposition extension.
  People who are interested in taking part in the code sprint: ...
• Anders Mörtberg: Maintenance work on the agda/cubical library
  We're planning to do some work on the agda/cubical library. The main things I want to do are:
  1. Merge/close old PRs and close/resolve old issues.
  2. Decide which definitions of integers and rational numbers are the best and reorganize the library a bit so that it's clearer which to use. This will probably involve creating a new "Numbers" package.
  3. Discuss and resolve issues related to the organization of the algebra code.
  Feel free to add any other ideas to this thread or discuss on Zulip.
  People who are interested in taking part in the code sprint: Anders, Evan, Max, ...

Social activities

• The Agda pub: Bring your own fancy beer and/or delicious pub food for a nice evening, and discuss whatever's on your mind!
• Virtual excursion: Hike or bike to a local beauty spot, share your pictures, and join us on Zoom for a relaxing morning/afternoon.

Wrap-up meetings

link