Blog by Lionel Parreaux, PhD Student @ EPFL
I am a 6th-year PhD student at EPFL, in the Data Analysis Theory and Applications Laboratory (DATA), and creator of the Squid type-safe metaprogramming library for Scala. My interests include: functional programming; dependent types; effect systems; compilers; metaprogramming; high-level program optimization; embedded domain-specific languages; query languages; database systems; verification; video games design and development; physics engines…
For me, programming languages are more than “just tools” to tell computers what to do; they are, equally importantly, vectors for expressing thoughts in a rigorous way, and for communicating these thoughts to other humans.
I would venture to say that good programming is not unlike good writing, and even sometimes resembles poetry. There is something beautiful in a tight, well-typed program clicking together fluently with the guarantee that it will not go wrong, keeping that promise throughout our changes and refactoring. And there is something unique in the humbling pleasure of having a compiler tell us, rightly, that we are wrong, and that we need to revise our mental model of a problem.
Of course, compilers are often wrong themselves, so it is one of my personal missions to make compilers less often wrong, and to make them more understandable and less frustrating when, unavoidably, they are.
I am not interested in abstraction for its own sake — my end goal has always been to build useful, practical software with a focus on correctness, maintainability, and performance.
High-level and especially functional programming languages offer good solutions to twe first two of these goals, but they typically incur a lot of runtime overhead, defeating the third one. Moreover, functional languages usually provide little in the way of controlling that overhead, so the only option is often to rewrite our programs in terms of more error-prone, lower-level abstractions.
As part of my research, I have developed new ways of regaining some control on the performance of functional programs, without giving up on high-level abstractions. I have worked on developing novel metaprogramming approaches extending the multi-stage programming discipline. As part of that effort, I am developing a staged database compiler which integrates seamlessly into Scala applications, removing the application/database impedance mismatch, while also leveraging traditional performance-oriented database implementation strategies.
I have recently been working on an innovative graph-based intermediate representation for optimizing functional languages, which can be used to partially-evaluation programs aggressively without having to rely on inlining and code duplication. One of the goals of this technique is to provide some hard guarantees on the removal of abstractions from user programs, so that one can develop abstract, modular code “without fear” and “without regret.”
The name of the blog, Well-Typed Reflections, is a pun on the double meaning of reflection, which is both the act of “engaging in serious thought or consideration,” and a metaprogramming technique. Since a central topic of my PhD has been to use type systems for making metaprogramming safer, I naturally prefer the latter activity to be well typed. But as a philosophical stance, I think we should also strive to make our everyday reflections “well typed” too, by applying the same kind of rigor and clarity that we use in formal methods to philosophy, politics, and societal issues.