PhD Course in Dependently Typed Functional Programming with Idris

Organiser:
Edwin Brady, University of St Andrews

Website:
Can be found here.

Lecturer:
Edwin Brady.

Dates of the course:
March 11, 12, 14 and 15, 2013.

Time:
Lecture 13:00-14:30, exercises 15:00-16:00.

Room:
TBA.

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

Program:
Lecture 1: A tour of Idris – Monday, 11 March, 13:00-14:30

• 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

Advanced reading: E. Brady: Programming in Idris: a Tutorial (2013)

Exercise Session 1: Monday, 11 March, 15:00-16:00

Lecture 2: Embedded Domain Specific Languages – Tuesday, 12 March, 13:00-14:30

• 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:
E. Brady and K. Hammond: A verified staged interpreter is a verified compiler
(2006)
E. Brady and K. Hammond: Resource-safe Systems Programming with Embedded Domain
Specific Languages (2012)

Exercise Session 2: Tuesday, 12 March, 15:00-16:00

Lecture 3: Effect management – Thursday, 14 March, 13:00-14:30

• 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:
E. Brady and K. Hammond: Resource-safe Systems Programming with Embedded Domain
Specific Languages (2012)
A. Bauer and M. Pretnar: Programming with Algebraic Effects and Handlers (2012)

Exercise Session 3: Thursday, 14 March, 15:00-16:00

Lecture 4: Implementing a Dependently Typed Language – Friday, 15 March, 13:00-14:30

• 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:
E. Brady, C. McBride and J. McKinna: Inductive Families Need Not Store Their
Indices (2004)
E. Brady and K. Hammond: Scrapping your Inefficient Engine: Using Partial
Evaluation to Improve Domain-Specific Language Implementation

Exercise Session 4: Friday, 15 March, 15:00-16:00

Exercises will cover the following:

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

Prerequisites:
Participants should be familiar with a functional programming language and the notion of pure
functional programming.

Exam:
Evaluation will be on a pass/fail basis, and the requirement for passing is active participation in the
lectures, discussions and exercises.

Credits:
4 ECTS

Amount of hours the student is expected to use on the course:
Participation: 12
Preparation: 6