<

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

Sophia Drossopoulou / Martin Odersky / Edwin Brady / Felienne Hermans / Gilad Bracha
Code Mesh V
05 Nov 2020
17.10 - 18.10

Panel discussion: Types for All: From weak to strong, from static to dynamic

When working from home, everyone looked at what books were on display on the shelves in the background. Type systems seemed to be very much in vogue, often put there to be seen. In order to not loose momentum, we are planning a panel on Type Systems at Code Mesh! It will be lead by Felienne Hermans of Leiden University. 

The idea is to discuss the panelists' approach to type systems, the rationale behind their design decisions, and how they have benefited the programming languages they have created. Questions will include, but not be limited to: when do we want type, when are types in the way, and what can we do about that? How extensible should a type system be? Attendees, through the Q&A section of the app, will be able to ask their own questions. With cameras on, don't forget to put your books on display. 

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
Edwin Brady
Code Mesh V
06 Nov 2020
17.30 - 18.10

TBA

TBA

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