Agda Implementors' Meeting XXXI

The 31st Agda Implementors' Meeting will take place in Edinburgh, Scotland from Thursday 10 November 2022 to Wednesday 16 November 2022. Note that AIMXXXI was initially planned for 2019 but got postponed due to COVID-19, whilst we had several online meetings XXXII-XXXV. The meeting will consist of:

  * Presentations concerning theory, implementation, and use cases of Agda and other Agda-like languages.

  * Discussions around issues related to the Agda language.

  * Plenty of time to work in, on, under or around Agda, in collaboration with other participants.

Twitch link where we stream the talks in the morning sessions.

Important dates

2022-10-21

Registration deadline

2022-11-10 (Thu) to 2022-11-16 (Wed)

AIM XXXI

Programme

All talks, coffee breaks and sprints take place on the ground floor of the Informatics Forum of the University of Edinburgh.

Talks

• Philip Wadler: Update on PLFA
• John Leo: Counterpoint Analysis and Synthesis. Update on the status of this project since the FARM 2022 presentation.
• Patrik Jansson: Dimension analysis and graded algebras
• Antoine Van Muylder: Extending cubical Agda with Internal Parametricity
• Jesper: Connecting Agda to other theorem provers via EuroProofNet (slides)
• Maximilian Doré: Filling cubes in Cubical Agda with poset maps
  When working with Cubical Agda, one often has to show that coherences hold by filling certain cubes. We’ll present how we can systematically come up with fillers for cubes using a characterisation of maps in Dedekind cubes as poset maps.
• Vikraman Choudhury: TBA
• Thorsten Altenkirch : TBA
• Andre Knispel: Axiomatic set-theory with ur-elements and its applications
• Joris Ceulemans: Sikkel: An Agda Library for Multimode (Simple) Type Theory
• Felix Cherubini: The solver for equations in commutative rings in agda/cubical
• Philipp Joram: Final Coalgebra Semantics in HoTT
  Final coalgebras of analytic functors exist classically. Let's use Cubical Agda to try and find them, constructively.

  https://github.com/phijor/agda-cubical-multiset
• (your talk here)

Discussion suggestions

• Andreas Nuyts: State of cubical agda and its library (Discussion + code sprint)
  • Working with constraints
  • Equality-in-equality-out category theory
  • (…)
• Philipp Joram: How to improve Agda's editor integration in 2022?
  I'd like to discuss how interaction with Agda could be improved. In particular, I'd like to explore how agda-mode can become more editor independent.
• Andreas Abel: Our feedback on GHC medium-term priorities
• Orestis Melkonian: CI tools for Agda
  Many of us use a home-grown CI setup for their Agda projects, time to unite!
• (your discussion here)

Code sprint suggestions

• John Leo: work on MusicTools; potential integration with Schmitty
• Marcin Jan Turek-Grzybowski: Modify the behavior of Refine (C-c C-r) command to allow for choosing constructors (PR #5889).
• Jesper:
  • Improving predictability and performance of instance search
  • Agda error index (similar to the Haskell one, see issue 659) (postponed to another AIM)
  • Work on 1.0 release of agda2hs (see open issues)
  • Controlled unfolding of abstract definitions (based on Controlling Unfolding in Type Theory, see also issue433)
• Guillaume: Compile time substitution of definitions
• Maximilian Doré: Implementing a tactic for Cubical Agda (currently in development here).
• Amélia Liao: Type-directed search for identifiers at prompt (like Coq's "Search") -- maybe next time
• Thorsten Altenkirch : Coinductive types with destructors -- sorry I had to cancel
• Lucas: Adding explicit positivity annotations to Agda
• Orestis Melkonian: Gather feature requests for setup-agda and try to implement them.
• Andreas Abel: Reflection binding/library with well-scoped de Bruijn indices
• Proposed by James - idea by 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: ...

• (your code sprint here)

Participants

• Orestis Melkonian
• James Chapman
• Jesper Cockx
• Andreas Nuyts
• Philip Wadler
• John Leo
• Fredrik Nordvall Forsberg
• Patrik Jansson
• Joris Ceulemans
• Antoine Van Muylder
• Philipp Joram
• Marcin Jan Turek-Grzybowski
• Guillaume Allais (part time)
• Xueying Qin
• Liam O'Connor
• Maximilian Doré
• Vikraman Choudhury - cancelled, sick
• Jacques Carette
• Josselin Poiret
• Amélia Liao
• Thorsten Altenkirch - cancelled
• Artem Shinkarov
• Andre Knispel
• James McKinna (part-time)
• Malin Altenmüller (part-time)
• Lucas Escot
• Andreas Abel
• Felix Cherubini
• Oskar Eriksson
• Sean Watters
• Henry Blanchette
• Mauro Jaskelioff
• Justus Matthiesen
• Tudor Ferariu
• (your name here)

Location

The meeting will take place in the ground floot of the Informatics Forum:

The rooms are located in the ground floor, just after you enter the building via the main doors. The building is access controlled, so you will have to sign in at the reception.

Excursion

There will be a day-long hike on Sunday, 13 November. We will walk (part of) the 9th stage of the famous John Muir Way. We will take a bus to the small village of Aberlady and walk from there to the beautiful seaside town of North Berwick, spanning a total of 13km/8miles and taking approximately 3-4 hours (check the map).

A tentative timeplan follows:

For any information/comments/questions/concerns, contact Orestis Melkonian.

More information will appear here.

Workspaces nearby

Here are a couple of University places to work near the Informatics Forum building where AIM will be held, in case you want to continue hacking after 5pm or on Saturday:

• Teviot Row House:

  • just opposite of the Forum, two separate options inside
  • New Amphion: weekdays 9am-7pm, Saturday 12pm-5pm
  • Library Bar: weekdays 12pm-1am, Saturday 12pm-1am

• Potterrow Dome: weekdays 9am-5.30pm

  • right next to Forum

• Pleasance Cafe: weekdays 9am-11pm, weekend 10am-11pm

  • slightly further away, but still in walking distance

If you find anything else, please post it here for other people to know!

About Edinburgh

Edinburgh is Scotland's compact, hilly capital. It has a medieval Old Town and elegant Georgian New Town with gardens and neoclassical buildings. Looming over the city is Edinburgh Castle, home to Scotland’s crown jewels and the Stone of Destiny, used in the coronation of Scottish rulers. Arthur’s Seat is an imposing peak in Holyrood Park with sweeping views, and Calton Hill is topped with monuments and memorials.

More information will appear here.

Accommodation

Here is a list of recommended hotels nearby:

• Edinburgh First
  Edinburgh First is the accommodation service of the University of Edinburgh and they offer good quality, well priced rooms at a number of locations in the City year round. If you book your accommodation via Edinburgh First, you can use the discount code 'EVENT' to receive a 15% discount.
• IBIS South Bridge
  This IBIS hotel is located five-minutes walk from the event. There is another IBIS at Hunter Square which is a little further away towards the city centre.
• 10 Hill Place
  This hotel is located two minutes from the event.
• Jury's Inn
  Jury's Inn is a ten-minute walk from the event and benefits from being very close to the railway station and the airport bus bus stop.
• Leonardo Boutique Hotel Edinburgh City
  This hotel is located on Lauriston Place and is a ten-minute walk from the event.
• Premier Inn
  This chain has a number of hotels close to the event, including Princes Street, East Market Street and Lauriston Place.
• Princes St Backpackers
  If you require budget accommodation, Princes St Backpackers is one of the most affordable hostels, and is about 20 minutes walk from the event.

Registration

You can register for the meeting by filling out the form below and emailing it to Orestis Melkonian.

    Registration form for Agda Implementors' Meeting XXXI

    Name:

    Title and optionally abstract (if you want to give a talk or lead a discussion):

    Suggestions for code sprints (optional):

    Dietary restrictions:

    Additional comments:

There is no registration fee. Coffee breaks will be included. Transportation, accommodation and meals are to be covered by the participant.

Last but not least, huge thanks to our sponsors:

GOLD:
SILVER:

Wrap-up notes

Nov.10

• agda2hs:
  • Update to work with Agda-2.6.3 release candidate
  • Initial attempts towards `-XBangPatterns`
• cubical tactic:
  • changes to cubical-agda to accommodate the tactic moving forward
• positivity:
  • exploratory discussions, gathered questions to ask the experts
  • issues with subtyping, similar to the erasure story
  • similarities with the existing notion of "polarity"
• reflection:
  • barely started changing the Agda reflection interface to have well-scoped terms
• model-checking:
  • decided on first steps, namely look at what is there now in Schmitty
• setup-agda:
  • some initial demonstration of the tool + some discussions/comparisons with existing tools
• cubical-docs:
  • detected some differences between the documentation and the actual behaviour of the code

Nov.11

• refine:
  • identified problems, so as to ask Andreas A.
• agda2hs:
  • fixed a bug with printing shadowed names (Agda was introducing suffixes)
  • working on a new check for Haskell identifiers (variables, constructors, ...) since Agda has less restrictions
  • some more documentation + stack support
  • usability suggestions (e.g. warning when using `f` which is an exported type variable)
• compile-time-substitutions:
  • some initial discussions, Guillaume has some draft/prototype using # REWRITE #
  • demo with map (f . g) and map id
• cubical-tactic:
  • progress using external solver (in Haskell), now need to properly parse the solver's output into Agda again
• strict-positivity:
  • figured out some theoretical issues
  • how to leverage existing "modalities" infrastucture
• setup-agda:
  • a lot of discussions on several different solutions (manual "pedestrian" version, omelkonian/setup-agda, wen-kokke/setup-agda, setup-agda-action)
• cubical-agda:
  • minor bugfixes
• other:
  • Andreas N. experimenting with SizedTypes and discovered issues

Nov.14

• refine:
  • expert feedback from Andreas, who identified some remaining issues that Marcin plans to fix tomorrow
  • then enquiry the AIM developers wrt. reusability
• agda2hs:
  • automatically generating imports
  • some new issues for the 1.0 release
  • settled on having do-notation by default, but user can use module `Dont` to retain explicit binds
  • automatically generating language extensions
• cubical-tactic:
  • talk in the morning on this topic exactly
  • working tactic using the reflection API (execTC, etc..)
  • still needs refining
• strict-positivity:
  • working modality for polarity `@++`
  • ongoing work on error messages
• reflection:
  • most work done in pub during the night :)
  • working prototype for well-scoped terms (i.e. `Term` now indexed by a `Nat`, and var becomes a `Fin`)
  • patterns still a bit flaky; not currently checking whether a pat.var. is introduced linearly
  • two directions: one that scope-checks an old-school plain `Term` to `Term n` and the inverse which forgets all scoping information
  • uploaded on the agda repo under `/notes/reflection/`
  • call to test existing reflection code and see if anything breaks
• cubical-agda:
  • whole discussion session at noon
  • possibly referring to 1lab from cubical-agda docs
  • a long list of action points for the immediate future
• abstract-unfolding:
  • parsing done! user can now declare an `abstract unfolding (A) where` block
  • next step: actually defining the unfolding behaviour within the enclosed block

Nov.15

• MusicTools
  • John gave a talk today and got helpful advice
• refine
  • Modified behavior of refine command:
    • suggests list of constructors from which you can pick one
    • automatically makes implicit arguments explicit if they are unsolved
    • automatically inserts holes for instance arguments that are not solved
    • autocompletion for constructor names
  • On branch intro-implicits-in-dt-constructors
  • Still unresolved issues with iterated refining and autocompletion. Help from Emacs experts wanted!
• agda2hs
  • Set up documentation + CI for building it
• positivity
  • work is still ongoing on integrating with existing positivity checker, fixing many bugs
  • fixing internal double-checker to handle modalities properly
  • discussed semantics of "strictly negative" and "strictly mixed"
• reflection
  • Guillaume tried out new well-scoped reflection API
• Agda CI
  • Had a discussion, plan to set up repository with template
• abstract unfolding
  • Implemented scope checker for `unfolding` statements
  • Currently working on computing transitive closure
  • Nothing is broken, but nothing is working
• proposal for new module system
  • (Very drafty) proposal for new module system
  • Comments are very welcome on Zulip

Nov.16

• agda2hs:
  • review on external PR that wants to do literal pattern matching on Naturals
  • documentation is live (added by newcomer Henry!)
  • Orestis failed to add feature for qualified imports
• strict-positivity:
  • presented demo with working μ, Free!!!
  • some features still missing (such as annotating a datatype parameter)
  • hints towards simplifying other modalities as well (irrelevance, etc..)
• scoped-reflection:
  • refactored well-scopedness from `Fin n` to a list of names, to prevent stupid arithmetic errors with DeBruijn indices
  • tested with intros/refine tactic by Guillaume, code stayed the same!
• setup-agda:
  • some people started using Wen's action
  • Orestis relinquished the name from his (deprecated) action
• abstract-unfolding:
  • working demo using Vec/Product!
  • currently unfolds the transitive closure
  • only supports individual names/identifiers, but not full modules
• lsp-agda:
  • Philipp demo'ed a working minimal demo that parses the current buffer and gives a response back to the user!
  • uses the Haskell `lsp` package and `Agda` as a library