Functional Geekery Episode 54 - Edwin Brady

In this episode I talk with Edwin Brady. We talk Dependent Types and Idris. We cover his background of getting interested in dependent types, getting up and going with Idris, how to participate to drive Idris forward, and much more.

Our Guest, Edwin Brady

@edwinbrady on Twitter
https://edwinb.wordpress.com/

Sponsors

This episode is sponsored by DailyDrip.com. Use the coupon `geekery` to save $5 on your first month, and make learning part of your daily routine with DailyDrip.com.

Announcements

PolyConf 2016 will be taking place on June 30th – July 2nd. Visit http://polyconf.com/ to keep updated with news as more details become available.

Curry On is taking place July 18th and 19th in Rome. Visit curry-on.org to find out more and to register.

Full Stack Fest will be hold in Barcelona on September 5-9th. You can check out 2016.fullstackfest.com —to find out more.

The Erlang User Conference is coming up in Stockholm, Sweden, the 6th through the 16th of September. Early Bird tickets are now available and get a 10% discount on the conference when you use the code: FunctionalGeekery10 when registering.

Destination Code, a new unconference starting in Utah, is having its inaugural event this December. Visit http://www.destination.codes/ to find out more.

If you have a conference related to functional programming, contact me, and I will be happy to announce it.

Topics

About Edwin Brady
Idris
How Edwin got into software development
Alan Bundy
Epigram
Edwin’s experience in industry before going for Ph.D.
Migrating code from Haskell to C++
How Edwin migrated from C++ to Dependent Types
Trying to write out data types in Python
Edwin’s preference between dynamic and static types
Type Driven Development
“Allowing more precision in types”
Being more explicit about assumptions up front
How does one get going with Idris
`printf` in C
Dynamic checks and what checks are required
“If you give the type up front you have a some hope of the machine figuring out the program for you”
Types as constraints similar and comparison to Prolog
Type Driven Development with Idris
“About taking types as the first thing you do”
Holes in Idris
Evolving code with help from evolving types
Edwin’s view of the Idris community’s adoption
Coq
Agda
shapeless library in Scala
Total Programs
What opportunities could people help participate in to move Idris forward
Idris’ backend plugin system
How to get up and running
David Christiansen’s M.Sc thesis
Jan de Muijnck-Hughes
Big Tech Day presentation in Munich
Idris on freenode
Idris mailing list
Idris on Github

As always, a giant Thank You goes to David Belcher for the logo design.

Episode source