Programming with dependent types (Seminar)

Winter semester 2015

Organization

Organizer	Yufei Cai AlumniYufei Cai
Weekly meeting	Tuesday 14:15-16:00 in Room C118a, Sand 14.
Language	English
Credits	4 or 3 LP (Im Vorlesungsverzeichnis)
Office hours	Monday 09:00–11:00, Thursday 09:00–11:00 in B211

Description

Dependent types are types that can depend on values: arrays of length 25, 20-by-20 matrices, or integers larger than -3. Agda and Idris are two dependently typed languages. Dependent types are good for many things—from eliminating ArrayIndexOutOfBoundsException to automatic generation of visitors—yet the idea itself originates from the foundational crisis of mathematics at the turn of the 19th century. Dependent types carry their own coding patterns and caveats. In this seminar, we learn to program effectively with dependent types: How to make hard things possible, how to not make simple things hard, and a bit of how things work under the hood.

Process

The seminar consists of a series of weekly presentations followed by a programming project.

Phase 1: presentations

During this phase, participants take turns presenting papers about programming with dependent types. The presenter’s job is to help the audience apply ideas in the paper in practice; s/he need not talk about everything in the paper. Live programming is recommended whenever appropriate. Each presenter should create or copy a programming exercise to drive the idea home. Other participants should do the exercise and mail the result to the next presenter.

The presenter has these responsibilities:

1. Understand one or more practicable ideas from the reading material and teach them to other participants.
2. Give a brief outline of the presentation at the end of the meeting one week earlier, so that those unfamiliar with the topic has time to prepare.
3. Discuss the previous programming exercise briefly.
4. Produce the next programming exercise.

The audience has these responsibilities:

1. Do the weekly programming exercise.
2. Help the presenter communicate by asking questions at the precise moment when they failed to understand something.
3. Offer additional insight.

Participants should submit finished exercises to the next presenter and to me before Sunday, 23:59:59.

Phase 2: final project

At the end of the semester, each participant should write a program making use of dependent types in nontrivial ways. It is an opportunity to combine concepts learnt throughout the semester, and to self-assess how effective a dependently typed programmer one manages to become. The scope of the project should be something you can program in a weekend. Participants should present their projects and submit a short paper.

Schedule

Basic topics

• Introduction
  • Brady. Idris, a general purpose dependently typed programming language: design and implementation.
  • Nordström, Petersson, Smith. Programming in Martin-Löf’s type theory.
  • Norell and Chapmann. Dependently typed programming in Agda.
• Visitors, folds, or compositional operations on datatypes
  • Altenkirch, McBride, McKinna. Why dependent types matter.
  • Augusteijn. Sorting morphisms.
• Views and propositional equality
  • McBride and McKinna. The view from the left.
  • Norell and Chapmann. Dependently typed programming in Agda.
  • Oury and Swierstra. The power of Π.
• Pre-/post-conditions, or proof-carrying code
  • Altenkirch, McBride, McKinna. Why dependent types matter.

Advanced topics

• Coinduction
  • Abel. Coinduction in Agda using copatterns and sized types. talk abstract
  • Jacobs and Rutten. A tutorial on (co)algebras and (co)induction.
• Universe construction
  • Altenkirch and McBride. Generic programming within dependently typed programming.
  • Norell and Chapmann. Dependently typed programming in Agda.
  • Oury and Swierstra. The power of Π.
• Embedding domain-specific languages
  • Altenkirch and Reus. Monadic presentations of lambda terms using generalized inductive types.
  • Brady and Hammond. Resource-safe systems programming with embedded domain specific languages.
  • Brady. Embedded domain-specific languages in Idris.
• Setoids
  • Barthe, Capretta, Pons. Setoids in type theory.
• Dependent pattern matching
  • Cockx, Devriese, Piessens. Pattern matching without K.
  • Coquand. Pattern matching with dependent types.
  • Goguen, McBride, McKinna. Eliminating dependent pattern matching.
  • Sozeau. Equations: a dependent pattern-matching compiler. [Slides]
• Type inference
  • Miller. Unification under a mixed prefix.
  • Norell and Coquand. Type checking in the presence of meta-variables.
• Formal presentations of type theory
  • Dybjer. Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics
  • Hoffmann. Syntax and semantics of dependent types.
  • McBride and McKinna. The view from the left.
  • Nordström, Petersson, Smith. Programming in Martin-Löf’s type theory.
• Mathematics and category theory
  • Barthe. Formalising mathematics in UTT: fundamentals and case studies.
  • Huet and Saïbi. Constructive category theory.
  • Nordström, Petersson, Smith. Programming in Martin-Löf’s type theory.

Free topics

The presenter is free to choose the reading material for these topics.

• Pure type systems

• Termination checking

• Universe polymorphism

Resources

• General proof theory (27–29 November 2015 in Tübingen)
• Type theory for vegetables
• Univalent foundations of mathematics, with an Agda overview
• Agda tutorial by Diviánszky Péter
• Operator precedence convention of HoTT-Agda
• The Agda manual of stubs. Feel free to contribute.