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
http://davidchristiansen.dk/
Conference Announcements
RacketCon is October 7th & 8th at the University of Washington, with keynote speakers Dan Friedman and Will Byrd. Visit http://con.racket-lang.org/ 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 http://2017.clojure-conj.org/ 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 http://www.lambda.world/.
CodeMesh is coming up November 8th and 9th in London. For more information, and to keep an eye open for registration, visit http://www.codemesh.io/.
Moonconf will be taking place the 9th-11th of November. For more information visit http://moonconf.org/.
Clojure SYNC will be taking place in New Orleans on February 15th & 16th of 2018. For more information and to register visit: http://clojuresync.com/.
LambdaDays 2018 will be taking place February 22nd and 23rd in Kraków, Poland. For more information, and to register, visit http://www.lambdadays.org/.
If you have a conference related to functional programming, contact me, and I will be happy to announce it.
Announcements
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 https://www.patreon.com/fngeekery.
Topics [@3:22]
About David
Idris
Indiana University Bloomington
Racket
Type Driven Development in Idris
The Type Theory Podcast
Dan Friedman on Functional Geekery
David’s introduction to programming and computers
MS-DOS GW-BASIC
Major in Philosophy with Minor in Computer Science
What put functional programming on David’s radar
Lisp
Haskell
A Gentle Introduction to Haskell
Structure and Interpretation of Computer Programs
PLTScheme, now Racket
Internship doing I.T.
QBasic
C
Perl
Smalltalk
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”
Nuprl
Jon Sterling’s jonPRL and RedPRL
Types as predicates that describe behavior
Agda
Coq
Typed Racket
Using Racket as a proof language for Nuprl type system
Logic for Computable Functions by Dana S. Scott
Robin Milner
Edinburgh LCF
ML
Running LCF style proofs in Racket macro-expansion
Hackett
cur
miniKanren
µKanren
Scribble
Slideshow
video
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.