Edwin Brady Tells Us What's New in Idris 2

Edwin Brady introduces Idris 2, demonstrating its interactive editing features, dependent types, and type-driven development of concurrent programs.

Idris is a functional programming language with first-class types and with built-in support for interactive editing. Together, these features mean that Idris is ideally suited to "Type-driven development," where we begin by writing a type and an empty function definition, then refine the definition to a complete working program. Recently, Edwin has been working on a new implementation, Idris 2, written in Idris itself (and now able to compile itself). In this talk, he'll give a tour of what's new in Idris 2, focusing in particular on interactive editing and type-driven development of concurrent programs. Edwin says, "I'll aim to make the talk accessible to those with some knowledge of functional programming, but not necessarily any knowledge of type systems. At the end of the talk, I hope that you'll have a new appreciation of what types can help you do!" Edwin is a Lecturer in Computer Science at the University of St. Andrews, interested in type theory, dependently-typed functional programming, compilers, and metaprogramming. When he's not rewriting Idris, you might find him playing Go (he's about 2nd kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. He regrets to inform you that he is also responsible for perpetrating the Whitespace programming language. This virtual talk was brought to you by the Berlin Functional Programming Group. Join us on Meetup: meetup.com/Berlin-Functional-Programming-Group/ Follow us on Twitter: twitter.com/BerlinFPGroup Buy a T-shirt: teespring.com/berlin-fp-group Support us on Patreon: patreon.com/bfpg