If you're here for AIM XXXIV in June 2021, please go to https://wiki.portal.chalmers.se/agda/Main/AIMXXXIV

The thirty-third Agda Implementors' Meeting will take place between 2020-10-12 and 2020-10-23. 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.

Important dates

2020-10-05

Soft deadline for registration

2020-10-05 to 2020-10-11

People can express interest in code sprints

2020-10-12 to 2020-10-23 (weekdays only)

AIM XXXIII

Registration

You register for the meeting by sending an email to Jesper, or 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 include this in your registration email.

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.

In contrast 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-xxxiii 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 2020-10-12

• 10-11: Introduction
• 11-12: Planning of discussions and code sprints
• 15-16: Talk by Wen Kokke: "Schmitty the Solver"

Tuesday 2020-10-13

• 10-11: Talk by Jesper Cockx: "Agda Core: Where do we come from and where do we go?" (slides)
• 11-11:30: Wrap-up meeting
• 15:00: Discussion: Improving interoperability of the libraries

Wednesday 2020-10-14

• 15-16: Talk by Jacques Carette and Jason Hu: "The new categories library for Agda"
• 16-16:30 16:30-17: Wrap-up meeting

Thursday 2020-10-15

• 10-11: Talk by Ulf Norell: "Programming with Universes for Fun and Profit"
• 11 12-13: Code sprint on Agda Core
• 13: A discussion about the structure identity principle (zoom)
• 14-15: Discussion (lead by Víctor López Juan): Twin types in Agda

Friday 2020-10-16

• 11-12: Talk+Discussion lead by Thorsten Altenkirch: "Coinduction in cubical agda"
• 15-16: Wrap-up meeting
• 16-: Social event: AIM XXXIII Pub

Saturday 2020-10-17

• 14 - ?: Social event: Virtual Excursion (TBA).

Monday 2020-10-19

• 10-11: Talk by Stefania Damato: "Constructing Simple and Mutual Inductive Types in Agda"
• 11-12: Discussion about Sized Types
• 15-16: Talk by James Chapman: "Higher Assurance Haskell: Using Agda to model and test a Haskell program (experience report)"
• 16-16:30: Wrap-up meeting
• 17:30-21: Social event: Dungeons & Chickens (organized by Jesper Cockx)

Tuesday 2020-10-20

• 10-11: Talk by Nicolai Kraus: "Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it?"
• 13-15: Work on Compiling Agda to Readable Haskell code sprint

Wednesday 2020-10-21

• 11-12: Continued discussion of sized types, hopefully culminating in implementation sketch
• There will be no talks this day, but attendants are encouraged to join the talks at SPLS. The code sprints and discussions will continue as normal.

Thursday 2020-10-22

• 10-11: Talk by Johannes Schipp von Branitz: "Displayed Univalent Reflexive Graphs in CTT"
• 11-11:30: Wrap-up meeting
• 15:30-17: (Not part of AIM but likely of interest.) Ambrus Kaposi: "Quotient inductive-inductive types and higher friends" HoTT Electronic Seminar

Friday 2020-10-23

• 11-12: Talk by Musa Al-Hassy: "Do-it-yourself Module Systems: Unbundling on the fly and mechanically obtaining term types from theories"
• 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.

Talk and discussion proposals

• Wen Kokke: Schmitty the Solver
  I recently published an Agda library called Schmitty, which provides flexible bindings between Agda and SMT-LIB solvers. In this talk, I'll go over the basic design of Schmitty, and propose several small extensions that would make excellent code sprints!
• Jesper Cockx: Agda Core: Where do we come from and where do we go?
  A recurring question people have about Agda is "why doesn't it have a proper core language?" In this talk, I'll discuss the current state of the internal double-checker of Agda, past attempts at formalizing more of Agda's theory (see https://github.com/agda/agda-spec), and how we could move towards having a proper core language for Agda in the future.
• Jacques Carette and Jason Hu: The new categories library for Agda
  Details TBA.
• Ulf Norell: Programming with Universes for Fun and Profit
  To write tactics or other meta-programs in Agda you need to manipulate reflected syntax--an Agda representation of the internal syntax of Agda itself. Its definition consists of a handful of mutually recursive datatypes representing terms, patterns, sorts, etc, and defining functions over these can be a bit awkward. In this talk I will show you some infrastructure for working with reflected syntax, and how using universes can make everything much nicer.
• Víctor López Juan: Twin types in Agda
  A discussion on how to add twin types to the Agda typechecker (see https://dl.acm.org/doi/abs/10.1145/3406089.3409030 for the theory, and https://github.com/agda/agda/pull/4605 for WIP code)
• Thorsten Altenkirch : Coinduction in cubical agda
  I want to discuss some issues with doing coinduction in cubical agda.
• Stefania Damato: Constructing Simple and Mutual Inductive Types in Agda
  A description of work done for my master's thesis, involving the construction of a framework in which we can express simple and mutual inductive types, and a starting point for a reduction from these types to W-types.
• Nicolai Kraus: Two-Level Type Theory (2LTT) - What is it, what can it do, and does Agda need it?
  2LTT is a small extension of dependent type theory and allows us to reason about strict (a.k.a. judgmental/definitional) equality semi-internally. I briefly want to talk about how this works, what one can do with it, why one would want to do that, and what (from my point of view) is still missing on the theoretical side. I only need 15min or so for the talk, but I hope we can afterward discuss whether other projects could benefit as well from 2LTT and what people's requirements would be.
• Johannes Schipp von Branitz: Displayed Univalent Reflexive Graphs in CTT
  A univalent reflexive graph (URG) on a type is a reflexive binary relation such that the canonical map idToRel is an equivalence. A displayed URG over a URG roughly consists of a type family where each fiber carries the structure of a URG, but the fields depend on the URG on the base type. A DURG induces a URG on the total type of its underlying type family, giving rise to a characterization of the identity types of the total type. I used them to prove the equivalence of strict 2-groups and crossed modules, but I will put the focus of the talk on the meta-theory of DURGs. The code can be found at #435 . My thesis is available here.
• Nils Anders Danielsson: Making different libraries interoperable and/or merging them
  Explanation.
• James Chapman: Higher Assurance Haskell: Using Agda to model and test a Haskell program (experience report)
  At IOHK we have a core language based on System F omega mu for our smart contract platform Plutus. We have an intrinsically typed implementation of an interpreter and type checker for this language in Agda. We compile the interpreter to Haskell and make use of the same Haskell libraries as the production implementation and also borrow the production parser and pretty printer. The Haskell executable serves as a reference implementation which we can test the production implementation against, on hand written examples, and on NEAT generated System F omega mu terms due to work by Wen Kokke. I will describe some details of the project and the experience of using Agda for this project and some thoughts on future applications.
• Musa Al-Hassy: Unbundling on the fly and mechanically obtaining term types from theories
  We show how a bit of reflection can be used to achieve on the fly unbundling to lift record fields to the type level as parameters, and we use monadic do-notation to make the resulting setup practical and pragmatic for experimentation. It is well known in the folklore that record types are contexts (i.e., sequences of name-type pairs), we go on to show that termtypes (GADTs) are also contexts. Moreover, since records and termtypes are both contexts, we show how to derive the latter from the former mechanically via a macro; e.g., we mechanically ask for the termtype of dynamic systems, monoids, pointed sets, collections and find the results to be that of the natural numbers, tree skeletons, the maybe type, and the list type. Surprisingly, the entire development is under 300 lines of Agda. Project webpage: https://alhassy.github.io/next-700-module-systems/

Code sprint proposals

List code sprint proposals here.

• Wen Kokke: Schmitty the Solver
  Schmitty provides flexible bindings between Agda and SMT-LIB solvers. There's a large number of possible extensions for Schmitty to make her even more useful! Right now, Schmitty supports the core theory, i.e., propositional logic, as well as integer arithmetic linked to Agda integers, and real arithmetic linked to Agda floats. However, the SMT-LIB standard offers so many more possibilities!
  • Add backends for other SMT-LIB compliant solvers (easy);
  • Add theory of real arithmetic linked to Agda rational numbers (easy);
  • Add theory of floating-point numbers linked to Agda floats (easy);
  • Add theory of strings linked to Agda strings (easy);
  • Add theory of sequences linked to Agda lists (moderate);
  • Add theory of uninterpreted functions and constants linked to Agda names (moderate);
  • Add theory of regular expressions linked to gallais/aGdaREP (moderate);
  • Add theory of algebraic datatypes linked to Agda datatypes (moderate);
  • Add theory of arrays linked to an axiomatisation of Haskell arrays (moderate);
  • Add support for combined theories (moderate);
  • Add support for logic declarations (moderate);
  • Add proof reconstruction for SAT using Kanso.SatSolver (moderate);
  • Add proof reconstruction for Z3 proofs (cf. Proof Reconstruction for Z3 in Isabelle/HOL) (hard).
  People who are interested in taking part in the code sprint: Wen, Jorge, Manuel, ...
• Anders Mörtberg: Cubical Agda and the agda/cubical library
  Hopefully other agda/cubical contributors can attend so that we can fix many of the issues and merge some of the open PRs.
  People who are interested in taking part in the code sprint: Anders, Marcus, Max, Martin, Marcin, Ulrik ...
• Jesper Cockx: More control over reduction for interaction & reflection
  Currently the Agda typechecker features only two main modes of reducing a term: either reducing it to weak-head normal form, or fully normalizing it. However, during interactive use it would often be nice to reduce just calls to a specific function, or to limit the set of allowed reductions in other ways. This code sprint will be about implementing the core mechanism for this in the Agda typechecker, and binding it to the reflection interface so it can be used in (both compile-time and edit-time) macros.
  People who are interested in taking part in the code sprint: Jesper, John, Kyle, Artem,...
• Arjen Rouvoet (proposing, not an expert): Distributing Agda
  I would like to discuss the channels via which we distribute Agda. It seems we heavily rely on cabal/stack for typical installations, which are not package managers and at least in my personal experience break for a variety of reasons, all the time. Is it feasible to produce binary distributions of Agda?
  People interested: Andreas
• James Chapman: Compiling to readable Haskell
  I would like to investigate creating a new compiler backend for Agda aimed at verifying Haskell programs that generates readable Haskell from a restricted subset of Agda. The intended use case would be using Agda to verify a key component in a Haskell project and then generating readable Haskell that can be easily integrated with the Haskell project.
  People interested: James, Andreas, Ulf
• Manuel Bärenz: Fixing sized types
  Sized types have bugs where you can prove bottom, essentially making them inconsistent or `--unsafe`, e.g. https://github.com/agda/agda/issues/2820. The very least that should be done is marking them as unsafe. But ideally, we'd fix the implementation. I (Manuel) don't know what the right theory is, but if experienced people can offer some guidance what the right approach is, I/we can attempt to fix it. The first step would be to meet and work out a sound theory on a virtual whiteboard. Then we can discuss implementation.
  People interested: Manuel, Andreas, Nisse, Andrea
• Ulf Norell: Quasiquoting for reflection
  Working with reflected syntax can be quite painful. The goal of this sprint is not to implement full quasi-quoting, but rather investigate how far we can get with the existing machinery and clever libraries, and if there are any low hanging fruits in terms of extensions that could make our lives easier.
  People interested: Ulf, Manuel
• Nils Anders Danielsson: Improving erasure support
  People interested: Nisse
• Johannes von Branitz: Displayed Univalent Reflexive Graphs
  People interested: Johannes, Ulrik
• Manuel Bärenz: Use more instances in the standard library
  It would be nice if instances like Show and Eq were implemented more in the standard library. They are fairly prevalent in `agda-prelude`, so maybe it is time to merge the prelude into the standard library, and refactor the latter accordingly.
  People interested: Manuel
• Proposer: Title
  Description
  People who are interested in taking part in the code sprint: ...

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.
• Dungeons & Chickens: In which I (Jesper) will host a game of Dungeons & Dragons on Discord for anyone who wants to join, no previous experience required. This game will be suitable for 1st level characters and might feature two very angry chickens named Agda and Coq.

Wrap up reports

See AIM XXXIII Wrap-ups