Agda Implementors' Meeting XXIII

The twenty-third Agda Implementors' Meeting was held at the University of Strathclyde in Glasgow, Wednesday 20 April to Tuesday 26 April 2016. The meeting was be similar to previous ones:

• 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.

Location

The meeting will take place in room LT1415 in Livingstone Tower of the university of Strathclyde in central Glasgow.

Programme

Wrap-up meeting summary

A short summary of the daily progress can be found here.

Talks

Jesper Cockx: A sound unification algorithm based on telescope equivalences [ slides, paper (draft) ]

Dependent pattern matching is arguably one of the best features of Agda. At the core of the algorithm for checking definitions by pattern matching lies a (first-order) unification algorithm. However, the implementation of this unification algorithm in Agda 2.4.* and earlier contains many additions that aren't considered in the literature on dependent pattern matching, such as postponing of equations and support for eta-equality of record types. This mismatch between theory and implementation has caused numerous bugs, see #292, #473, #635, #1071, #1406, #1408, #1411, #1427, #1435, #1497 and #1613. In this talk, I will present a new way to think about unification by representing unification problems as telescopic equations, and unification rules as equivalences between these telescopes. This representation lies directly at the base of the new implementation of the unification algorithm in Agda 2.5.1.

Henning Basold: Towards a Theoretic Foundation of Agda's Data Types [ slides ]

In recent years, increasingly many people have become interested in using Agda as a proof assistant. So it becomes desirable that we have a formal proof that Agda as a logic is consistent and that we can point to models of for it. This has been done for some parts of the language. The most recent example of which is probably the proof of strong normalisation of the copattern language for (non-dependent) sized types by Andreas Abel et al. Also, many features of Agda and their combination have been investigated in the context of other type theories, most notably pure type theories.

In this talk, I will focus on one feature that has not been investigated in other contexts: dependent mixed inductive-coinductive data types. First, I will present a syntax based on (co)recursion schemes, and prove subject reduction and strong normalisation for its reduction relation. This language and a few basic properties have also been implemented Agda. Next, we will see how these data types and their rules correspond to closure of fibrations under certain initial and final dialgebras, and how we obtain models of such categories. The latter is actually the origin of the presented language. Finally, I would like to discuss the steps that remain to obtain a formalised core language.

The first part is joint work with Herman Geuvers for LICS'16. The second part is based on a paper I presented last year at FICS.

Andreas Abel: Introduction to Agda source code [ bug fixing notes ]

This talk attempts to give an overview over some parts of the Agda source code (333 Haskell modules, 100kloc). We touch on different representation of the abstract syntax and the parsing/scope-checking/type-checking/compilation pipeline. You do not need to be a Agda contributor yet to follow this talk, it serves also as a first orientation when getting to work on a code sprint.

Ulf Norell: Type checker reflection [ code ]

Recently I had the pleasure of serving on David Christiansen's PhD committee where I got the chance to study the cool things he's been doing with reflection in Idris. I particularly liked his elaborator reflection, which provides an interface to the elaborator from Idris metaprograms. So, naturally I stole his ideas and put them in Agda. The result is a new type checking monad with primitive operations that provide access to the Agda type checker. In this talk I'll show you the new interface and some fancy tactics programming that we couldn't do before.

Conor McBride: A Cubical Crossroads [ board 1 board 2 board 3 board 4 ]

I'll explore how far we can get when constructing a cubical type theory with canonicity, without committing either to nontrivial proof relevance (e.g., Univalence) or to nontrivial proof irrelevance (e.g., K). I hope to shed some light on the design space.

Anton Setzer: Writing GUIs in Agda using Objects [ Agda Code (html)Agda code on git (main file main.agda), paper (draft), ooAgda Library (github) ]

Joint work with Andreas Abel and Stephan Adelsberger

We introduce a library for writing interactive programs in Agda which make allow to create GUIs. The interactive programs will be able to use some aspects of objects. When creating GUIs in the most advanced versions the creation of GUIs is similar to how it is done in Java by creating and object which has as methods action listeners. A small GUI example will be demonstrated.

James McKinna: Bidirectional transformations are proof relevant bisimulations, moreover graded as a (bi-)category over the bicategory of relations [ Complements Witness Consistency paper and DBTX talk abstract (from Bx2016@ETAPS) ]

I'll attempt to motivate, define, and hopefully explain, the terms in the title, and establish a proof of the claimed result.

Guillaume Allais: Type and Scope Preserving Semantics [ slides, paper and code on Github ]

We introduce a notion of type and scope preserving semantics generalising Goguen and McKinna’s approach to defining one traversal generic enough to be instantiated to renaming first and then substitution. Its careful distinction of environment and model values as well as its variation on a structure typical of a Kripke semantics make it capable of expressing renaming and substitution but also various forms of Normalisation by Evaluation as well as, perhaps moresurprisingly, monadic computations such as a printing function.

We then demonstrate that expressing these algorithms in a common framework yields immediate benefits: we can deploy some logical relations generically over these instances and obtain for instance the fusion lemmas for renaming, substitution and normalisation by evaluation as simple corollaries of the appropriate fundamental lemma.

Edwin Brady: Programming with Effects in Idris

I'll talk about the current status of the Idris effects library. The effects library allows Idris programmers to define side-effects via algebraic data types, and track the resource usage of effectful operations in their types. I'll show how we can use this to define resource usage protocols (e.g. file management and network communications) in the type system, and give some examples.

Excursion to Arran

We meet at Glasgow Central Station 8.20 (under the clock in the middle) in order to take the 8.40 train to Ardrossan, where we change to the ferry to Brodick on Arran. It is possible to buy a combined train and ferry return ticket all the way to Brodick for £15.80.

On Arran, we will catch bus 324 10.55 to Brodick Castle, where we will climb Goatfell. Bring lunch and sensible clothes and shoes!

The ferry back to Ardrossan leaves from Brodick 16.40 or 19.20.

Travel to Glasgow

By train

See National Rail for trains within the UK. Both Glasgow Central and Glasgow Queen Street Station are within walking distance of the University of Strathclyde.

People on the continent can take the Eurostar to London, and then take another train to Glasgow. See also The Man in Seat 61 for more information.

By plane

The closest airports are Glasgow International Airport (30 minutes bus connection (bus 500) to George Square), Edinburgh Airport (1 hour bus connection (Citylink Air) to Buchanan Bus Station) and Glasgow Prestwick Airport (40-50 minutes train connection to Glasgow Central).

Accommodation

A convenient place to stay is the Glasgow City Centre Premier Inn, just across the road from the University of Strathclyde. It might also be worth considering Airbnb. If you are going the bed and breakfast route, note that Strathclyde is located in the Merchant City area of central Glasgow.

Registration

To register, please fill out this form.

Participants

• Ulf Norell (University of Gothenburg)
• Fredrik Nordvall Forsberg (University of Strathclyde)
• Jesper Cockx (KU Leuven)
• Conor McBride (University of Strathclyde)
• James Chapman (University of Strathclyde)
• Yijun Yu (The Open University)
• Stuart Gale (ExtractMethod Ltd / University of Strathclyde)
• Andrea Vezzosi (Chalmers University of Technology)
• Guillaume Allais (Radboud University Nijmegen/University of Strathclyde)
• Víctor López Juan (Chalmers University of Technology)
• Nils Anders Danielsson (University of Gothenburg)
• Andreas Abel (University of Gothenburg)
• James McKinna (University of Edinburgh)
• Peter Hancock (University of Strathclyde, retired)
• Anton Setzer (Swansea University)
• Edwin Brady (University of St Andrews)
• Stephan Adelsberger (Vienna University of Economics)
• Robert Atkey (University of Strathclyde)
• Sam Lindley (University of Edinburgh)
• Henning Basold (Radboud University Nijmegen)
• Shayan Najd (University of Edinburgh)
• Danel Ahman (University of Edinburgh)
• Craig McLaughlin (University of Edinburgh)

Code Sprint Ideas

• Overloaded projections (Andreas)
• Layout in records and pattern matching lambdas (Ulf) (and do-notation?)
• Record patterns in Lambda (Guillaume)
• Tactics programming (Ulf can help)
• Optimization: if you have Agda code that is suspiciously slow, contact Nisse
• Some improvements to the new unifier (Jesper)
• Phantom types for reflected syntax (Jesper)
• Fuse coverage checking and clause lhs checking (Jesper)
• Scoped comments: having scoped-checked/type-checked code in comments (Guillaume)
• Documenting and cleaning up the ooAgda library; objects, GUIs and interactive programs (Anton)
• Creating more advanced examples of GUIs in Agda (Anton)
• Heroic documentation sprint (Fredrik)
• Explicit substitutions (Fredrik, James)
• Cubical Type Theory (Issue 1703) (Andrea)
• Standard library (Andreas)
• Warnings (Andreas)
• reStructuredText support for literate Agda: Make documentation fun to write and typecheckable (Víctor)
• Elm-style error messages

Wishful thinking:

• Cumulativity (Conor)
• Observational equality (Conor)
• Prop à la OTT (Guillaume)

Nice if someone does it:

• Static binary generation using Travis (Guillaume)

Sponsorship

This meeting is supported by the Scottish Informatics and Computer Science Alliance.