Programming with dependent types (Seminar)
Winter semester 2015
Organization
Organizer  Yufei Cai ResearcherYufei Cai 
Weekly meeting  Tuesday 14:1516: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, 20by20 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:
 Understand one or more practicable ideas from the reading material and teach them to other participants.
 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.
 Discuss the previous programming exercise briefly.
 Produce the next programming exercise.
The audience has these responsibilities:
 Do the weekly programming exercise.
 Help the presenter communicate by asking questions at the precise moment when they failed to understand something.
 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 selfassess 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
13/10  Background and organization slides homework 
20/10  Basic language features (Yufei) script homework 
27/10  Visitors, folds, or compositional operations on datatypes (Jona) script homework 
03/11  Views and propositional equality (David) Abel’s slides script 
10/11  Pre/postconditions, or proofcarrying code (Sebastian) merge sort list properties van Laarhoven 
17/11  Inductive relations and syntax overloading (Yufei) prolog stlc homework 
24/11  Coinduction (Ingo) coinduction copattern sized types 
01/12  Universe construction (Sebastian) show database functor 
08/12  Dependent pattern matching (Paolo) typed de Bruijn indices 
15/12  Normalization by evaluation (Tillmann) code 
12/01  No meeting 
19/01  No meeting 
26/01  Inductive families in type theory (David) Dybjer 97 Dybjer 91 De Bruijn 91 
23/02  Project presentation 
Basic topics
 Introduction
 Brady. Idris, a general purpose dependently typed programming language: design and implementation.
 Nordström, Petersson, Smith. Programming in MartinLö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/postconditions, or proofcarrying 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 domainspecific languages
 Altenkirch and Reus. Monadic presentations of lambda terms using generalized inductive types.
 Brady and Hammond. Resourcesafe systems programming with embedded domain specific languages.
 Brady. Embedded domainspecific 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 patternmatching compiler. [Slides]
 Type inference
 Miller. Unification under a mixed prefix.
 Norell and Coquand. Type checking in the presence of metavariables.
 Formal presentations of type theory
 Dybjer. Inductive sets and families in MartinLöf’s type theory and their settheoretic semantics
 Hoffmann. Syntax and semantics of dependent types.
 McBride and McKinna. The view from the left.
 Nordström, Petersson, Smith. Programming in MartinLö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 MartinLö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 HoTTAgda
 The Agda manual of stubs. Feel free to contribute.