Agda Implementors' Meeting XXIV

The twenty-fourth Agda Implementors’ Meeting will be held at the University of Utrecht, from Monday October 10 to Friday October 14 2016.

The meeting will consist of a mix of talks and code sprints:

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

If you would like to attend, please fill in the registration form here:

https://goo.gl/forms/uzkXvEaHxDJHznWm2

Location

The meeting will take place at the university campus "De Uithof", a.k.a Utrecht Science Park. More specifically, in the building of the Computing Science departement on the 5th floor – the building is called "Buys Ballotgebouw".

From the central train station of Utrecht you can take either bus lines 12 or 28 to De Uithof. Both take around 15 minutes to reach the campus. After getting out of the bus, the easiest way to find our building is to aim for a 7-storey high concrete flat with the words "Universiteit Utrecht" and the university logo on the rooftop.

• If travelling on line 12, the closest stop to our building is called "Padualaan".
• If travelling on line 28, the closest stop to our building is called "Botanische Tuinen".

Staying in Utrecht

The Science Park (de Uithof) is a bit outside of the city center. There are several good options nearby, including:

• Hotel Mitland (http://www.mitland.nl/) - conveniently located between the Science Park and city center
• Stay OK Bunnik (https://www.stayokay.com/en/hostel/utrecht-bunnik) - a hostel nicely located in the forests near the Science Park

If you need any more specific advice, please contact the organizers.

Travel to Utrecht

• By train:
  • From Belgium/France/UK, take the Intercity Brussels to Rotterdam Central and once in Rotterdam change train towards Utrecht Central.
  • From Germany, there is a direct ICE train from Düsseldorf to Utrecht, taking about 2h.
  • For route planning, it's very handy to use the website called 9292.nl.
• By airplane:
  • The big airlines all land at Amsterdam Schiphol Airport. There's a train station immediately under the arrivals hall, and a direct train between Schiphol and Utrecht Central takes 25 minutes.
  • Rotterdam Airport and Eindhoven Airport are the destination of some low-cost carriers, such as Transavia, Wizz Air and RyanAir. A trip from either airport to Utrecht involves a combination of shuttle bus and train. Great information on route planning can again be found on 9292's special airport page.

Getting around in Utrecht / Public transport in the Netherlands

• Utrecht is not really big, so you can walk pretty much anywhere close to the center in up to 30min.
• If you want to use public transportation, remember the nation-wide route planner: 9292.nl.
• The OV-Chipkaart
  • A single NFC card is used throughout the whole Netherlands to pay for any kind of public transport, it's called OV-Chipkaart.
    • If you plan to travel 7 single journeys or more by bus in Utrecht, than it's cheaper to buy the OV-chipkaart than paying cash.
    • An OV-Chipkaart can be bought at the ticket machines with blue sign in any train station in the Netherlands.
• Bikes
  • The easiest (also cheap) way to move around the city and enjoy more freedom is to rent a bike. Some places to rent a bike for a week are:
    • Both pretty close to the station, in ascending distance:
    • Laag Catharijne (€7,50 / day)
    • Willemstraatbike (€7,00 / day)
    • If you rent for a whole week, it will be usually cheaper than paying 7 times the day fare.

Program

 Programme

Code Sprints

• AA: Record declaration rewrite (nested parametrized modules) -- Never started.
• JC: Export REWRITE rules (UN: similar to display pragmas) -- Never started.
• JC: Well-scoped internal syntax through GADTs. Do a substantial experiment first (pattern matching, unification, meta-variables). See Edward Kmett's "bound" library, investigate GHCs dependently typed features, see also prototype on msp-strath github. -- Some experiments done.
• FNF: Better positivity error highlighting. -- Done and pushed to stable!
• WS: Interaction command for "with". -- Initial investigation.
• UN: Super classes (design and implementation). -- Done! Even documented!
• GA: Warnings: deprecation and other non-fatal warnings. -- Done! For instance, only warning on BUILTIN NATURALZERO.
• VLJ: "Unify infrastructure for errors/warnings of parser and type checker." ! Done
• NAD: Equational reasoning is slow: can we have tactics for controlling the flow of information? -- Done. No tactics. But with flipped arguments of transitivity it became up to 5x faster.
• NAD/UN: Don't normalize before quoting. (1h code sprint) -- Done! Turned out to require some parameterization on whether we should normalize or not.
• NAD: agda --latex slow because of deserialization. Invoke agda --latex from emacs (similar to compile). -- Done!
• NAD: abort an interactive command without losing state issue #????. -- Only discussion. Wrote a paper instead.
• Make GHC-backend (so-called "MAlonzo") output well-typed Haskell code. -- Wilco Kusee does this as a master.
  • Typed compiler frontend!? Typed CompiledClause, typed TreeLess!?
• GA: Ocaml backend. (Laziness?!) -- Not started.
• AA: Quantitative typing (Conor's "plenty of nuttin'"). -- Never started.
  • Stop abusing the ..-modality!? Replace it by 0-modality of Conor!?
• VLJ: Syntax highlighting in the documentation (.rst). -- Proof of concept of what info should be generated.
• JC: Unquoting of data types for ornaments in Agda. -- Nothing. (Improve unquoteDecl: needs names for the scope checker).
• JC: Postponing left hand side checking. -- Probably nothing.
• JC: "Cannot instantiate"-horror error message improvement. -- May take a while.
• WS: Integrate tactics into interaction (IDE). -- Just an idea.
• WS: Facilities to debug tactics (verbosity). -- UN: ported Text.PrettyPrint to Agda, see Ulf's github.