Functional Geekery Episode 108 – David Christiansen

In this episode I talk with David Christiansen. We talk his introduction to functional programming, research in dependent types, Idris, Nuprl and LFC traits, work to add dependent types to macro-expansion in Racket, and much, much more.

Our Guest, David Christiansen

@d_christiansen on Twitter

Conference Announcements

RacketCon is October 7th & 8th at the University of Washington, with keynote speakers Dan Friedman and Will Byrd. Visit for more information and to register.

Celebrate the 10th anniversary of the release of Clojure October the 12th – 14th at the Clojure/Conj in Baltimore, Maryland. Visit for more information and to register.

LambdaWorld will be taking place in Cadiz, Spain on October 26th and 27th. For more information visit and to keep updated visit

CodeMesh is coming up November 8th and 9th in London. For more information, and to keep an eye open for registration, visit

Moonconf will be taking place the 9th-11th of November. For more information visit

Clojure SYNC will be taking place in New Orleans on February 15th & 16th of 2018. For more information and to register visit:

LambdaDays 2018 will be taking place February 22nd and 23rd in Kraków, Poland. For more information, and to register, visit

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


Some of you have asked how you can support Functional Geekery, in that vein,
Functional Geekery now has a Patreon Page.

If that is one of the ways you would like to show your support, you can
find out more at

Topics [@3:22]

About David
Indiana University Bloomington
Type Driven Development in Idris
The Type Theory Podcast
Dan Friedman on Functional Geekery
David’s introduction to programming and computers
Major in Philosophy with Minor in Computer Science
What put functional programming on David’s radar
A Gentle Introduction to Haskell
Structure and Interpretation of Computer Programs
PLTScheme, now Racket
Internship doing I.T.
David’s grad school work
Exposure to Idris at St Andrew’s summer school
General ML exposure around Copenhagen
False dichotomy between industry and “academic” languages
Progression to push into dependent types
“Part of my job description at the time was: learn about interesting things”
The Type Theory Podcast
Software Foundations
Adam Chlipala on Functional Geekery
Dependent Types as a aesthetic thing
Type Driven Development
Interactive programming environments from the 80’s
“Let the computer do what the computer is good at, which is the details”
Jon Sterling’s jonPRL and RedPRL
Types as predicates that describe behavior
Typed Racket
Using Racket as a proof language for Nuprl type system
Logic for Computable Functions by Dana S. Scott
Robin Milner
Edinburgh LCF
Running LCF style proofs in Racket macro-expansion
Resources to get started understanding dependent types
Software Foundations
Upcoming _Little Schemer_ family book on dependent types with Dan Friedman
Little Schemer
Upcoming talks previewing book at RacketCon and CodeMesh
Oregon Programming Languages Summer School videos
Suggestions for a title in Little Schemer tradition

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

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.