David Thrane Christiansen
-
Personal: david at davidchristiansen dot dk
I want programming to be a creative dialog between human and machine, where human creativity is aided by a mechanical attention to detail. To do this, I work with advanced type systems, metaprogramming, and domain-specific languages. In particular, I wrote a fair bit of the first version of Idris, and I’ve worked with Dan Friedman on making dependent types more accessible through The Little Typer.
I am the Executive Director of the Haskell Foundation. I used to work at Deon Digital in Copenhagen, Denmark and Galois in Portland, Oregon, USA. Before that, I was a postdoc with Sam Tobin-Hochstadt at Indiana University in Bloomington, Indiana. I completed my Ph.D. at the IT University of Copenhagen, Denmark, in January 2016 under the supervision of Peter Sestoft. Before getting married, I was known as David Raymond Christiansen.
The Little Typer
Dan Friedman and I wrote book on dependent types in the tradition of The Little Schemer. It was released on September 18, 2018.
Publications
Dependently Typed Haskell in Industry (Experience Report) (pdf)
In Proc. of 24th International Conference on Functional Programming (ICFP ’19)
Berlin, Germany, August, 2019
A description of challenges and benefits from dependently typed Haskell at Galois.
Extensible Type-Directed Editing (pdf)
In Proc. of the Workshop on Type-Driven Development (TyDe)
St. Louis, Missouri, USA, September, 2018
Idris’s interactive editing features are now extensible in Idris itself.
Efficiency of a good but not linear nominal unification algorithm (pdf)
In Workshop on Unification (UNIF)
Oxford, England, July, 2018
Faster nominal unification using a hybrid named-nameless representation of terms
Sequential Decision Problems, Dependent Types and Generic Solutions (pdf)
In Logical Methods in Computer Science 13(1)
A generic solver for sequential decision problems, in Idris
Elaborator Reflection: Extending Idris in Idris (pdf, acm, video)
In Proc. of 21st International Conference on Functional Programming (ICFP ’16)
Nara, Japan, September, 2016
Making the elaboration facilities available for metaprogramming in Idris
Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level Reflection (pdf, acm)
In Proc. of 26th International Symposium on Implementation and Application of Functional Languages (IFL ’14)
Boston, Massachusetts, USA, October, 2014
A means of implementing quasiquotation in the context of a type-directed tactic-driven elaborator
Pension Reserve Computations on GPUs (pdf, acm)
In Proc. of Workshop on Functional High-Performance Computing (FHPC ’14)
Gothenbug, Sweden, September, 2014
A description of generation of fast GPU code for solving the Thiele’s differential equations, generated from a high-level description of a class of life insurance and pension products
Dependent Type Providers (pdf, acm)
In Proc. of Workshop on Generic Programming (WGP ’13)
Boston, Massachusetts, USA, September, 2013
A mechanism for allowing datatype indices to be about something outside the language
Banana Algebra: Compositional Syntactic Language Extension (pdf)
In Science of Computer Programming, Vol. 78(10), Elsevier, 2013
Software Development for the Working Actuary (pdf, poster)
In Proc. of 4th International Symposium on End-User Development (IS-EUD ’13)
Copenhagen, Denmark, June, 2013
A short paper describing ongoing research and associated poster
Formal Semantics and Implementation of BPMN 2.0 Inclusive Gateways (pdf)
In Proc. of Web Services and Formal Methods (WS-FM ’10)
Hoboken, New Jersey, USA, September, 2010
Manuscripts
The Final Pretty Printer (pdf)
An extensible pretty printer with semantic annotations and proportional-width fonts
Reflect on Your Mistakes! Lightweight Domain-Specific Error Messages (pdf)
Presented at TFP 2014, Soesterberg, The Netherlands, May, 2014
A mechanism for displaying error messages for embedded languages using the terms of the embedded language rather than the host language
Selected Talks
Predictable Macros for Hindley-Milner (pdf, video)
Presented at TyDe 2020
Bidirectional Type Checking (video)
Presented at C∘mp∘se 2019
A Little Taste of Dependent Types (video)
Presented at flatMap(Oslo) 2018
A Little Taste of Types (video)
Presented at Code Mesh 2017
Elaborator Reflection: Extending Idris in Idris (video)
Presented at ICFP 2016
A Pretty Printer that Says What it Means (video)
Presented at Haskell Implementors’ Workshop 2015
Coding for Types: The Universe Pattern in Idris (video)
Presented at Curry On 2015
Type Providers and Error Reflection in Idris (video)
Presented at Compose 2015
Tool Demonstration: An IDE for Programming and Proving in Idris (pdf)
Presented at DTP 2014
An Actuarial Programming Language for Life Insurance and Pensions (pdf)
Presented at ICA 2014
Teaching
-
Instructor for Dependent Types at Portland State University, Spring 2019.
-
Instructor for Dependent Types at Indiana University, Spring 2017.
-
TA for Programmer som data (Programs as Data), Fall 2014, Fall 2013, Fall 2012, and Fall 2011
-
A week-long intensive course on Scala and DSLs at Chalmers in December, 2012
-
TA for Advanced Models and Programs, Spring 2011 (as M.Sc. student)
-
TA for Introduktion til scripting, databaser og systemarkitektur (Introduction to Scripting, Databases and System Architecture), Spring 2011 (as M.Sc. student)
Projects
My current project is Klister, an exploration of how to make hygienic procedural macros type-aware, while still providing a predictable programming model.
I’m a contributor to the first version of Idris, a functional programming language with full dependent types. In particular, I’m to blame for Idris’s take on type providers, quasiquotation, and the reflected elaborator.
I am a co-author and maintainer of the Idris IDE for Emacs, which attempts to unite the interaction styles of SLIME, agda-mode, and ProofGeneral, and to be a practical environment for writing runnable code using dependent types.
At IU, I worked on integrating proofs with macro expansion with Sam Tobin-Hochstadt.
Ph.D. and M.Sc. Theses
I defended my Ph.D. thesis, Practical Reflection and Metaprogramming for Dependent Types, on January 7, 2016. It describes a suite of metaprogramming features for Idris, including a means of quoting Idris’s core language using high-level Idris syntax, a way to rewrite error messages that arise from embedded languages, and a reflection of Idris’s elaborator into a monad with effects in the type checker.
My M.Sc. thesis (Danish speciale) describes Idris’s type providers, which allow dependent types to talk about values obtained from effectful computations that can observe the world in which the program finds itself being typechecked.
Miscellaneous
I’ve created some tutorials in connections with my teaching duties. In case they are useful outside of the specific courses for which they were designed, they are now online.
I’m a co-host of The Type Theory Podcast.
I’m a fluent user of English and Danish. I can also get by in Swedish and Esperanto, if necessary.