Main /
\ Main

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.

Links and Technology

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

There is also a Discord channel that may optionally be used for some impromptu code-sprints and discussion, which you can join at https://discord.gg/5wNVzVk. However, please keep all text-based communication on Slack.

Links to Zoom or similar systems can be found in the programme below.

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-05-25

First session (Zoom):

  • 10-11: Introduction
  • 11-12: Discussion: Matthew Daggitt: Implementing refactoring tools for Agda

Second session (Zoom):

Tuesday 2020-05-26

First session (Zoom):

  • 10-11: Talk: Andrea Vezzosi: Inductive Families in Cubical Agda

Second session (Zoom):

  • 13-14: Discussion: Jesper Cockx: Revising Agda's module system

Wednesday 2020-05-27

First session (Zoom):

  • 10-11: Discussion: Thorsten Altenkirch: The future of cubism
  • 11-11:30: Wrap-up meeting

Second session (Zoom):

  • 15-16: Talk: Jesper Cockx: To infinity, and beyond! On the need for sorts bigger than Setω

Thursday 2020-05-28

First session (Zoom, Twitch):

Friday 2020-05-29

First session (Zoom, Twitch):

  • 11-12: Talk: Arjen Rouvoet: Typed Compilation with Labels, without Trouble, and using Partial Commutative Monoids

Second session (Zoom, Twitch):

  • 15-16: Talk: Artem Shinkarov
  • 16-16:30: Wrap-up meeting (report)
  • 16.30-: AIM XXXII Pub (in zoom breakout rooms, bring your own beverages)

Saturday 2020-05-30

14 - ?: Virtual Excursion. People go to beauty spot nearby. Zoom (15) Upload pictures (with comments) to google photo gallery.

Monday 2020-06-01

First session (Zoom, Twitch):

  • 12-13: Talk/discussion: Nils Anders Danielsson: Some tricks for making Agda code faster ("slides")
  • 13-13:30: Wrap-up meeting (report)

Second session (Zoom):

  • 15-16: Discussion: Stephan Adelsberger and Anton Setzer: Combining Agda with external tools (details, code sprint, slides)

Tuesday 2020-06-02

First session (Zoom):

Second session (Jitsi, Twitch):

  • 15-16: Talk: Uma Zalakain: π with leftovers: a mechanisation in Agda

Wednesday 2020-06-03

First session (Zoom):

  • 12-13: Talk: Joris Ceulemans: Shallowly Embedding Type Theories in Agda as Presheaf Models (code, slides)
  • 13-13:30: Wrap-up meeting

Thursday 2020-06-04

First session (Zoom, Twitch):

  • 10-11: Talk: James Wood: Why does Dec look funny these days?

Second session (Zoom):

  • 15:30-16:30: Discussion: Fashionable mathematics, is it possible? The accessibility of Agda to mathematicians (learning curve, documentation and areas of Mathematics not covered)

Collaborative wrap-up pad

Friday 2020-06-05

First session (Zoom):

  • 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+3
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
Filippo SestiniUTC+2
Alex RiceUTC+1
Ayberk TosunUTC+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: Shallowly Embedding Type Theories in Agda as Presheaf Models
    Presentation of work in progress on a shallow embedding of (modal) type theories in Agda using presheaves.
  • Arjen Rouvoet: Typed Compilation with Labels, without Trouble, and using Partial Commutative Monoids.
    Intrinsically verifying type-preservation of a compiler is made difficult by jumps. Compilers invent fresh labels on demand and may use them before they are bound to a target instruction. To ensure type-preservation of the compiler, we need to witness that all labels that are used are indeed bound to an instruction of the appropriate type. We give a nameless encoding of labels and a co-contextual typing of bytecode. This enables writing a stateless, well-typed compiler where labels can be manipulated as first-class values. This is made possible by a hierarchy Relation.Ternary for programming with ternary relations in Agda.
  • 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. Perhaps this can turn into a discussion.
  • Filippo Sestini: Hacking setoid equality in Agda
    The goal of this talk is to give an overview of Setoid Type Theory as recently developed by Altenkirch et al., and to show a couple of possible ways to encode the notion of equality of such system into Agda, using the infrastructure of rewrite rules.
  • 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 (slides,tiny Agda fragments)
    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 (slides, code sprint)
    1. Interface which allows to add external tools (e.g. SAT solvers, model checkers, other decision procedures) to Agda, integrating work by Karim Kanso. (discussion)
    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. (code of Karim's thesis, git repository with the Agda fork of Karim, PhD thesis by Karim, Publication by Karim and Anton about this project).
    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 (discussion)
    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 the code of Karim's thesis, 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.
    Result of Code Sprint: Wen Kokke implemented calls to arbitrary function at type checking type with the requirement for external functions to be registerd: Git repository agda-exec-tc.
  • Stephan Adelsberger and Anton Setzer: Updating of the GUI libraries
    The goal of this small code sprint is to update the libraries for writing GUIs in Agda to the current version of Agda. A project over the summer will be to unify those libraries into a uniform framework for writing GUIs. Links: git repositories ooAgda, PPDP18, SETTA18, FeatureAgda; demo, papers Adelsberger/Setzer.

Wrap up reports

2020-05-29

  • Compiler for cubical agda (Andrea, Nisse)
    Nisse is doing a demo: erasure, some equivalences using erased proofs in the moment cubical features can't be compiled. Not clear how to compile because reduction appears under binders for I-variables. Need to remember coercion coming from univalence.
  • Revising the module system (Jesper)
    No work on this. But Jesper worked on sorts and instance search. Fixed bug on instance sorts but there are more problems. See instance issue
  • Tactics in std lib (Jesper)
    Jesper started discussion. Functions for substitution and application on reflected syntax needed.
  • Evaluation (Ulf)
    Never had an emacs function to compute weak head normal form, now triple C-u C-c C-n
  • Pretty printing interface (Guillaume B.)
    Pretty print agdai files, available on the pretty-print-interfaces branch. Usage agda --pretty-print-interface=abc.txt abc.agda. Why are cubical functions visible even if we don't use cubical? Needed in case the module is imported from a cubical module. Andreas: inspired by Guillaume cleaned up some code for show in Haskell. show vs pretty.
  • Cubical families (Thorsten)
    Need to merge SSet and cubical (families); with and paths; trouble with stable - advice use mutual definition or make an instance for Maybe. Thank you
  • Typed pattern synonyms (Fred,James,Guillaume A.(missing))
    Some syntactic issues. Don't yet check the types but do everything else. Infix synonyms possible.
  • Ordinal notations (Fred)
    Nothing happened yet.
  • Destructors (Thorsten)
    Nothing happened yet.
  • Whitespace library (James)
    uses stack with different versions.

2020-06-01

Only minor progress over the weekend

  • pattern synonyms 
 missed the details
  • whitespace (Ed) 
 main agda needs fast flag, using 8.10.1 under windows crashes
  • coinductive families (Thorsten) 
 rabbit hole : commutativity of coinductive addition

 with and interval variables. Jesper volunteers to fix this. not.

 discussion about cubical and sized types.

 Andrea is going to merge cubical with strict sets.

2020-06-03

  • erased constructors (Nisse)

in erased contexts surjectivity is equivalent to erased surjectivity. Improvement on this.

Looked at Quotients and erasure.

Andrea is working on the backend for a compiler with erased constructors.

  • Reflected syntax (Jesper)

Artem's request, needed telescopes to reflecting patterns.

Valid ordering of telescopes for reflected syntax.

unquoting not yet fixed.

big proof of equality for reflected syntax almost finished.

  • External tools (Ulf)

Did a bad thing: you can run any binary at compile time. Will have to register the apps.

Some discussion: what if this is not really a function?

Put it into TC? - can only run it as a tactic.

  • Busy beaver challenge (Andreas)

How to make agda slow. Example: ambiguous parse trees.

New label on the bug tracker

  • Cubical and conat (Thorsten)

discussion on how to implement commutativity for + on conats.

T. is still waiting for a version of cubical+sset

  • typed pattern synonyms (Ed)

progress but now most is broken.

2020-06-05

  • Anton has updated his gui library to the latest version of agda codesprint gui update
  • Debugging agda (Andreas)

So far done by adding print statements (possible since agda is very imperative and uses IO)

Use haskell's pretty-show tool. Can view values and collapse, expand.

See issue with info

(Some discussion on what format to use for manuals: rsd vs markdown).

  • GitHub actions (Ed)

Continued Integration runs triggered github pushes or by pull requests.

How do we use CIs? Do people check locally or do they use CIs?

Hitting the GitHub limits (run on MS servers for free).

(We are using travis and GitHub for integration tests.)

Proposal: only run CI on main branches but not on issue branches?

Further discussion on pull request

  • Slow unification example (Andrea) (issue 1625)

Flag : "--experimental-lossy-unification". Loose uniqueness of solutions. Andreas suggests "—experimental-first-order-unification"

(problem with implicit function spaces if you use -no-syntactic-equality-check can't use it on the standard library).

(Mysterious meme: agda-3)

(some discussion on implicit function types: should they be first order?)

  • with with path-types (andrea)

it wasn't as hard as Andreas thought.

T: Should boundaries part of the type. A: would need a lot of changes.

Nisse: redTT has better support of boundaries.

Andreas suggests to remove constraints generated by boundaries (otherwise there is a duplication). Concern that may be inefficient.

Q : this is merged in the development version. However, inductive families is not yet merged because injectivity is not yet addressed.

  • compiling erase constructors (Nisse)

example using quotients works. problem compiling non-erased higher constructors.

idea: can compile only things reachable from main.

  • typed pattern synonyms (james)

Discussions. Still in the middle of implementing this.

left hand sides not yet handled. Should be done soon.

  • adding telescopes to reflected classes (Jesper)

J. may write a conversion guide because it breaks old code.

Discussion on what to do with changes that are not backward compatible.

Discussion on tactics in the standard library yesterday.

  • Feedback on virtual meeting

Advantages of virtual meeting. How to mix?

Wen on next meeting in Edinburgh. Cannot be before next Spring.

  • extecTC (Wen)

inspired by discussion on Karim's work but also by desire to do things on neural networks.

a primitive that allows to execute any program in the TC monad (for type checking)

need to add allow programs to a file.

not allowed to use in safe mode. Needs "--allow-exec".

Git repository agda-exec-tc.

  • tactics in standard library (Ulf)

implemented printf for type errors. printf will be in the standard library?

  • conat addition commutativity (Thorsten)

different ways to prove this, discussion on different representation

proof doesn't go through the termination checker. Could be fixed by inline trans and allow that hcomp is size preserving.

Edit | History | Recent Changes (all) | Search
Page last modified on October 24, 2020, at 09:38 am
Powered by PmWiki