Secrets of type driven program synthesis - Edwin Brady | Lambda Days 2021

Edwin Brady demonstrates how Idris uses dependent types to interactively synthesize program fragments from type definitions.

This video was recorded at virtual Lambda Days conference, which took place on 16-19th February 2021 - lambdadays.org/lambdadays2021 Secrets of type driven program synthesis by Edwin Brady ABSTRACT Idris is a functional programming language with first-class types, where types may be parameterised by other values. This gives the language implementation a lot of information up front about what a function should do, which means we can use Idris is our interactive assistant, where we write programs by conversation with the machine. As part of this, we are actively developing program synthesis tools, which generate fragments of programs from types. This can appear like magic! However, the key ideas are surprisingly simple. In this talk, I will demonstrate the current state of program synthesis and Idris, and try to demystify how it works, as well as discuss some related work and possible future research directions. • Follow us on social: Website: lambdadays.org​ Twitter: twitter.com/LambdaDays​ • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: codesync.global • SUBSCRIBE TO OUR CHANNEL youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOw SPEAKER - Edwin Brady Creator of the Idris programming language 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. --- Lambda Days Website: lambdadays.org​ Twitter: twitter.com/LambdaDays​