Eberhard Karls Universität Tübingen

Mathematisch-Naturwissenschaftliche FakultätProgramming Languages and Software Technology

Programming with dependent types (Seminar)

Winter semester 2015

Organization

Organizer Yufei Cai
Researcher
Yufei 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

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-/post-conditions, or proof-carrying 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 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
  • 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