<

Edwin Brady

Creator of the Idris programming language; Lecturer

Edwin is Lecturer in Computer Science at the University of St Andrews in Scotland, interested in type-driven development, domain-specific languages and reasoning about effectful programs.

When he's not doing that, he might be playing Go, watching cricket, or wandering around Scotland's hills.

Upcoming Activities

Edwin Brady
Code Mesh V
Tutorial/ 05 Nov 2020
16.00 - 19.30

An Introduction to Idris 2

Idris (https://idris-lang.org) is a functional programming language with first-class types. It encourages “type-driven development”, where we begin by giving a type and an empty function definition, and refine the definition – with the machine’s help – to a complete working program. This tutorial will introduce a new implementation - Idris 2 – and show how its new features facilitate the correct implementation of complex protocols (e.g. of the sort found in communicating concurrent systems). Assuming some background in typed functional programming, I will introduce type-driven development, show how to use types to captures functional properties of programs, and show how to use linear types to implement safe concurrent communication protocols.

 

EXPERTISE

Intermediate functional programmer

 

COURSE DURATION

Half day

 

TARGET AUDIENCE

Programmers with some experience of a typed functional language (e.g. ML, Haskell)

PREREQUISITES

  • Some basic knowledge about types: function types, polymorphic types, algebraic data types
  • Programming with recursive functions
  • Understanding of higher order functions

 

OBJECTIVES 

  • Understand foundations of functional programming with first-class types
  • Be able to formally reasoning about program properties
  • Represent protocols in types

 

COVERS THE FOLLOWING TOPICS

  • Types as first-class constructs (dependent types)
  • Program synthesis via types
  • Quantities: erasure and linearity
  • Equality proofs
  • Protocols via linearity

 

 WHY YOU SHOULD ATTEND THIS COURSE

  • It will teach you how to use types to structure programming, not only in Idris but in other typed languages
  • It will show you what is possible in a modern programming language with an advanced type system

Past Activities

Edwin Brady
Code Mesh LDN 2018
09 Nov 2018
15.25 - 16.10

Idris 2: Type-driven development of Idris

We've had lots of fun over the last couple of years investigating the possibilities and limitations of type-driven development in Idris. 

As we write larger programs, though, we're finding the implementation of Idris is showing the strain - such is the nature of "research quality software." Edwin recently decided the time was right to start again and implement Idris 2 in Idris. 

In this talk, Edwin will give an introduction to type-driven development (in Idris 2) and report on progress so far, showing off the most interesting features which the new design enables (notably, linear types and better type inference).