Dependently Typed Functional Programming with Idris - 2013

Lecturer

Edwin Brady is a Lecturer in Computer Science at the University of St Andrews.

Description
Dependently typed functional programming has been an active area of research in programming languages for some time now. Edwin Brady, one of the leading researchers in the field, will provide an introduction to dependently typed functional programming using the Idris language. Topics to be covered include:
  • Language features such as dependent pattern matching, tactic-based proof scripts, and totality checking
  • Embedded domain-specific languages in Idris, including the unique techniques enabled by the presence of dependent types
  • Managing different kinds of effects without the inconvenience of Haskell's monad transformers
  • How to efficiently implement a dependently typed language, including an detailed discussion of the Idris typechecker and compiler.
The topics will be illustrated with examples and there will be exercise sessions following each lecture.


Prerequisites
Participants should be familiar with pure functional programming in a statically typed language.

Please have Idris installed on your computer if you plan to participate in the exercise sessions.

Videos


Slides and videos from the course are now available.

Course Plan

Each lecture will be followed by an exercise session from 15:00 to 16:00.

Lecture 1: A tour of Idris
Monday, 11 March, 13:30-14:30 in room 3A18

How to install

Why dependent types?
  • Functional and extra functional correctness
  • Verification
  • Generic programming
  • A survey of dependently typed programming languages - why Idris?

Introductory examples:
  • Vectors
  • Finite sets
  • Heterogeneous lists

Theorem proving
  • Properties of Nat
  • Inductive proofs and tactic scripts
  • Totality checking
  • Default arguments

A quick tour of language features
  • case, problems with dependent case
  • The with rule
  • Extended example: Binary arithmetic

Advance reading:

Lecture 2: Embedded Domain Specific Languages

Tuesday, 12 March, 13:30-14:30 in room 3A08

What is a domain specific language?
  • A brief history of programming languages and abstractions

Example: A well-typed interpreter, and some programs

Syntactic support for DSLs:
  • Syntax rules - if/then/else, bindings (e.g. for), pattern/term syntax
  • dsl notation

Interlude: System interaction
  • foreign functions, C bindings
  • Example: File IO

Resource aware programming
  • What is a resource?
  • A DSL for resource management

Advance reading:

Lecture 3: Effect management

Thursday, 14 March, 13:30-14:30 in room 4A20


The Haskell Approach: Monads
  • A monadic evaluator
  • Problems with monad transformers

Algebraic effects
  • State, IO, Exceptions, Random numbers
  • Eff: An Embedded DSL for effect management
  • Writing handlers for effects
  • Example: a stateful and effectful evaluator

The Eff interpreter
  • Tracking resources
  • Simple automated theorem proving
  • Syntactic sugar

Advanced examples:
  • Reasoning about effects and resource usage
  • Multithreading

Advance reading:

Lecture 4: Implementing a Dependently Typed Language

Friday, 15 March, 13:30-14:30 in room 4A14

The Core Type Theory (TT) and its metatheory
  • Properties
  • Typing rules

Tactics and elaboration
  • The development calculus
  • The Elaboration monad
  • Primitive tactics
  • Elaborating data types and functions
  • Elaborating high level constructs: where, with, case, type classes

Compilation
  • Phase distinctions
  • Forcing, collapsing and type erasure
  • Partial evaluation

Advance reading:

Exercises

An exercise sheet is now available. Exercises include:

  • vector equivalents of list functions (e.g. take, drop, reverse)
  • matrix multiplication
  • implementing views
  • well-typed interpreter: adding features
  • building a mini imperative DSL, with assignment, while, for
  • making new effects - nondeterminism, cgi, OS/interaction, multithreading

Example Code

The sample code from the lectures, and supporting code for the exercises.

Exam

Evaluation will be on a pass/fail basis, and the requirement for passing is active participation in the lectures, discussions and exercises. The course is worth 4 ECTS.

Acknowledgments

This course is supported by the IT University PhD School and the Actulus research project, funded in part by the Danish Advanced Technology Foundation (HTF).