I'm a Haskell/Rust programmer who lives in Cambridge with my wife Emily and son Henry (who has grown up a little since the photo on the right was taken). I have a PhD in Computer Science from York University, working on making functional programs shorter, faster and safer. Since then I've worked at Credit Suisse, Standard Chartered, Barclays Bank and Digital Asset, and I currently work at Meta — but all content and opinions are my own. I'm a strong believer in the functional programming approach, finding the combination of conciseness, static-typing and testability to offer significant advantages. I've got a blog mostly about Haskell, and I'm also on Threads, Twitter, LinkedIn and GitHub. To get in touch email me at ndmitchell@gmail.com.
Open Source Projects
At work, I am a major contributor to the Buck2 build system. At home, I develop a number of open source Haskell projects, all of which can be found at my Github page or on Hackage. I welcome both contributions via pull requests and bug reports via the GitHub issue trackers. Some of my more popular projects include:
- Shake - a library for writing build systems, an alternative to
make. - Hoogle - a Haskell API search engine, searching the standard Haskell libraries by function name and type signature.
- HLint - a tool that suggests stylistic improvements to Haskell code.
Papers and talks
All papers and talks are listed below, most recent first. Show all abstracts or citations.
Talk: Somewhat dynamic build systems
Slides, citation, abstract from S-REPLS 14, 07 Mar 2024.
@misc{mitchell:buck_07_mar_2024 ,title = {Somewhat dynamic build systems} ,author = {Neil Mitchell} ,year = {2024} ,month = {March} ,day = {7} ,note = {Presentation from S-REPLS 14} ,url = {https://ndmitchell.com/downloads/slides-somewhat_dynamic_build_systems-07_mar_2024.pdf} }
Abstract: The classic model of a build system, as presented in Build Systems a la Carte, is a single dependency graph. But in practice, large-scale build systems such as Bazel and Buck2 have two main dependency graphs - a target graph, and an action graph which refines the target graph. Both graphs can vary on the static vs dynamic spectrum (or alternatively, applicative vs monadic), giving either increased analysability or increased expressiveness.
In this talk we'll show the analysability requirements necessary to implement an efficient system to test the modified subset of a project. We'll also show the expressiveness requirements necessary to implement various language rules including Python, OCaml and Haskell. We then show how making the graphs dynamic in just the right ways gives us both, and have implemented these features in the Buck2 build system.
Build systems like Buck2 have two dependency graphs.
Talk: Buck2: optimizations and Bxl
Slides, video, citation from Bazel Community Day 2023, with Chris Hopman, 23 Oct 2023.
@misc{mitchell:buck_23_oct_2023 ,title = {Buck2: optimizations and Bxl} ,author = {Neil Mitchell and Chris Hopman} ,year = {2023} ,month = {October} ,day = {23} ,note = {Presentation from Bazel Community Day 2023} ,url = {https://ndmitchell.com/downloads/slides-buck2_optimizations_and_bxl-23_oct_2023.pdf} }
Introduction to Buck2 and Bxl extension language.
Talk: Accelerating builds with Buck2
Slides, video, citation, abstract from Developer Productivity Engineering (DPE) Summit 2023, 21 Sep 2023.
@misc{mitchell:buck_21_sep_2023 ,title = {Accelerating builds with Buck2} ,author = {Neil Mitchell} ,year = {2023} ,month = {September} ,day = {21} ,note = {Presentation from Developer Productivity Engineering (DPE) Summit 2023} ,url = {https://ndmitchell.com/downloads/slides-accelerating_builds_with_buck2-21_sep_2023.pdf} }
Abstract: Buck2 is an open-source build system written in Rust and designed to make your build experience faster and more efficient. Buck2 is extensible, allowing new languages to be added, but already has support for most popular languages (Python, C++, Rust, Go etc.). Thousands of developers at Meta already use Buck2, where we observed that Buck2 completed builds 2x as fast as Buck1, and developers using Buck2 ended up producing meaningfully more code.
In this talk we’ll discuss what makes Buck2 fast, what it shares with similar build systems (like Buck1 and Bazel), and what sets it apart. In order to give maximum performance Buck2 has a focus on parallelism, minimal invalidation on changes, integration with remote execution (running steps of the build on servers) and integration with virtual file systems. In order to have the flexibility to keep making improvements, we have a strong separation between the core build system (written in Rust, no knowledge of any language) and the language-specific rules (written in Starlark).
Buck2 is open source, and this talk will also cover what it looks like to get started with Buck2 in your project. More details about Buck2 can be found at https://buck2.build/.
Why Buck2 is fast
Talk: Buck2 for OCaml Users and Developers
Slides, video, citation, abstract from OCaml Users and Developers Workshop 2023, with Shayne Fletcher, 09 Sep 2023.
@misc{mitchell:buck_09_sep_2023 ,title = {Buck2 for {OCaml} Users and Developers} ,author = {Neil Mitchell and Shayne Fletcher} ,year = {2023} ,month = {September} ,day = {9} ,note = {Presentation from OCaml Users and Developers Workshop 2023} ,url = {https://ndmitchell.com/downloads/slides-buck2_for_ocaml_users_and_developers-09_sep_2023.pdf} }
Abstract: Buck2 is an open-source large scale build system used by thousands of developers at Meta every day. Buck2 can be used to build OCaml with some useful advantages over alternatives (e.g. Dune or Bazel). In this talk we’ll discuss what those advantages are, why they arise, and how to use Buck2 for your OCaml development.
Using OCaml in Buck2
Paper: Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows
Paper, citation, abstract, with Alexander Bernauer, Sofia Faro, Rémy Hämmerle, Martin Huschenbett, Moritz Kiefer, Andreas Lochbihler, Jussi Mäki, Francesco Mazzoli, Simon Meier and Ratko G. Veprek, 07 Mar 2023.
@inproceedings{mitchell:daml_07_mar_2023 ,title = {Daml: A Smart Contract Language for Securely Automating Real-World Multi-Party Business Workflows} ,author = {Alexander Bernauer and Sofia Faro and Rémy Hämmerle and Martin Huschenbett and Moritz Kiefer and Andreas Lochbihler and Jussi Mäki and Francesco Mazzoli and Simon Meier and Neil Mitchell and Ratko G. Veprek} ,year = {2023} ,month = {March} ,day = {7} ,url = {https://arxiv.org/pdf/2303.03749.pdf} }
Abstract: Distributed ledger technologies, also known as blockchains for enterprises, promise to significantly reduce the high cost of automating multi-party business workflows. We argue that a programming language for writing such on-ledger logic should satisfy three desiderata: (1) Provide concepts to capture the legal rules that govern real-world business workflows. (2) Include simple means for specifying policies for access and authorization. (3) Support the composition of simple workflows into complex ones, even when the simple workflows have already been deployed.
We present the open-source smart contract language Daml based on Haskell with strict evaluation. Daml achieves these desiderata by offering novel primitives for representing, accessing, and modifying data on the ledger, which are mimicking the primitives of today's legal systems. Robust access and authorization policies are specified as part of these primitives, and Daml's built-in authorization rules enable delegation, which is key for workflow composability. These properties make Daml well-suited for orchestrating business workflows across multiple, otherwise heterogeneous parties.
Daml contracts run (1) on centralized ledgers backed by a database, (2) on distributed deployments with Byzantine fault tolerant consensus, and (3) on top of conventional blockchains, as a second layer via an atomic commit protocol.
Introduction to DAML programming language and ledger.
Paper: Forward Build Systems, Formally
Paper, citation, abstract from CPP 2022, with Sarah Spall and Sam Tobin-Hochstadt, 17 Jan 2022.
@inproceedings{mitchell:rattle_17_jan_2022 ,title = {Forward Build Systems, Formally} ,author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt} ,year = {2022} ,month = {January} ,day = {17} ,booktitle = {Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs} ,pages = {130–142} ,doi = {https://doi.org/10.1145/3497775.3503687} ,url = {https://ndmitchell.com/downloads/paper-forward_build_systems_formally-17_jan_2022.pdf} }
Abstract: Build systems are a fundamental part of software construction, but their correctness has received comparatively little attention, relative to more prominent parts of the toolchain. In this paper, we address the correctness of forward build systems, which automatically determine the dependency structure of the build, rather than having it specified by the programmer.
We first define what it means for a forward build system to be correct - it must behave identically to simply executing the programmer-specified commands in order. Of course, realistic build systems avoid repeated work, stop early when possible, and run commands in parallel, and we prove that these optimizations, as embodied in the recent forward build system Rattle, preserve our definition of correctness. Along the way, we show that other forward build systems, such as Fabricate and Memoize, are also correct.
We carry out all of our work in Agda, and describe in detail the assumptions underlying both Rattle itself and our modeling of it.
A proof that Rattle is correct.
Paper: Implementing Applicative Build Systems Monadically
Paper, citation, abstract from Submitted to a conference that got cancelled due to COVID-19, with Bob Yang, 01 Jan 2022.
@inproceedings{mitchell:build_01_jan_2022 ,title = {Implementing Applicative Build Systems Monadically} ,author = {Bob Yang and Neil Mitchell} ,year = {2022} ,month = {January} ,day = {1} ,url = {https://ndmitchell.com/downloads/paper-implementing_applicative_build_systems_monadically-01_jan_2022.pdf} }
Abstract: Build systems are typically driven by a user script, e.g. the build system Buck is driven by BUCK fles. Mokhov et. al.classied build systems as either applicative or monadic, based on whether the build system required static dependencies, or allowed dynamic dependencies, respectively. Buck does not allow dynamic dependencies, so is classified as applicative.
In this paper we show that applicative build systems are only applicative from the perspective of the user, and are internally actually monadic. In particular, the actions executed are entirely dependent on the values in the user script. Following this observation, we rewrote Buck, an "applicative build system", using a monadic incremental computation engine, and saw improvements in both code complexity and performance.
How otherwise applicative build systems often need a monadic dependency graph
Talk: Rattle - simpler builds for smaller use cases
Slides, video, citation, abstract from Build Meetup 2021, 25 Jun 2021.
@misc{mitchell:rattle_25_jun_2021 ,title = {Rattle - simpler builds for smaller use cases} ,author = {Neil Mitchell} ,year = {2021} ,month = {June} ,day = {25} ,note = {Presentation from Build Meetup 2021} ,url = {https://ndmitchell.com/downloads/slides-rattle_simpler_builds_for_smaller_use_cases-25_jun_2021.pdf} }
Abstract: When writing a build system using a tool such as Bazel/Buck, much of the developers time is spent specifying dependencies between targets. The Rattle build system takes a different approach, omitting dependencies entirely, just requiring the build steps to be presented in a valid order. Rattle then uses file system tracing to infer the dependencies between commands, and (unlike previous systems such as Fabricate or Memoize) automatically infer parallelism. While Rattle isn't suitable at large scale, it can be used on projects as large as Node.js successfully, even rebuilding faster than the existing Make based build system.
Introduction to the Rattle build system
Talk: Cheaply writing a fast interpreter
Slides, video, citation, abstract from Performance Summit London Edition II, 23 Feb 2021.
@misc{mitchell:interpreter_23_feb_2021 ,title = {Cheaply writing a fast interpreter} ,author = {Neil Mitchell} ,year = {2021} ,month = {February} ,day = {23} ,note = {Presentation from Performance Summit London Edition II} ,url = {https://ndmitchell.com/downloads/slides-cheaply_writing_a_fast_interpreter-23_feb_2021.pdf} }
Abstract: For dynamic languages, there are well known approaches to achieve maximum performance, e.g. JIT. But such approaches are often very expensive to implement and maintain. In this talk we'll look at ways of implementing interpreters for less frequently used languages, which necessarily trade off performance vs implementation effort. As an example, we will consider the Starlark configuration language, a deterministic subset of Python used by the build systems Buck and Bazel. We'll cover techniques such direct AST interpretation, bytecode, closure generation - comparing the effort and performance of each approach.
Writing a fast programming language interpreter without generating assembly code.
Paper: Build Scripts with Perfect Dependencies
Paper, video, citation, abstract from OOPSLA 2020, with Sarah Spall and Sam Tobin-Hochstadt, 18 Nov 2020.
@inproceedings{mitchell:rattle_18_nov_2020 ,title = {Build Scripts with Perfect Dependencies} ,author = {Sarah Spall and Neil Mitchell and Sam Tobin-Hochstadt} ,year = {2020} ,month = {November} ,day = {18} ,booktitle = {Proceedings of the ACM Programming Languages 4, OOPSLA} ,articleno = {169} ,pages = {28} ,doi = {https://doi.org/10.1145/3428237} ,url = {https://ndmitchell.com/downloads/paper-build_scripts_with_perfect_dependencies-18_nov_2020.pdf} }
Abstract: Build scripts for most build systems describe the actions to run, and the dependencies between those actions - but often build scripts get those dependencies wrong. Most build scripts have both too few dependencies (leading to incorrect build outputs) and too many dependencies (leading to excessive rebuilds and reduced parallelism). Any programmer who has wondered why a small change led to excess compilation, or who resorted to a clean step, has suffered the ill effects of incorrect dependency specification. We outline a build system where dependencies are not specified, but instead captured by tracing execution. The consequence is that dependencies are always correct by construction and build scripts are easier to write. The simplest implementation of our approach would lose parallelism, but we are able to recover parallelism using speculation.
A forward build-system called Rattle that infers dependencies with tracing.
Talk: Migrating HLint to the GHC API
Slides, video, citation, abstract from MuniHac 2020, 11 Sep 2020.
@misc{mitchell:hlint_11_sep_2020 ,title = {Migrating {HLint} to the {GHC} {API}} ,author = {Neil Mitchell} ,year = {2020} ,month = {September} ,day = {11} ,note = {Presentation from MuniHac 2020} ,url = {https://ndmitchell.com/downloads/slides-migrating_hlint_to_the_ghc_api-11_sep_2020.pdf} }
Abstract: HLint is over 14 years old. Over the last 14 years we've changed license, project name, source control, configuration and much more besides. But until recently, HLint had always used the haskell-src-exts library for parsing Haskell. That parser was forked from the GHC parser 16 years ago, and as GHC has accumulated 16 years worth of bug fixes and features, the amount of Haskell code that could be parsed by GHC but not HLint increased. The obvious solution was to use the GHC API for parsing. In this talk I'll describe why we were so reluctant to move to the GHC API, how we decoupled HLint from GHC versions with ghc-lib, and how to change almost every line in a large project, without breaking anything or stopping ongoing development.
How and why we changed HLint to the GHC API parser.
Paper: Building an Integrated Development Environment (IDE) on top of a Build System (Revised)
Paper, citation, abstract from IFL 2020, with Moritz Kiefer, Pepe Iborra, Luke Lau, Zubin Duggal, Hannes Siebenhandl, Javier Neira Sanchez, Matthew Pickering and Alan Zimmerman, 04 Sep 2020.
@inproceedings{mitchell:hls_04_sep_2020 ,title = {Building an Integrated Development Environment {(IDE)} on top of a Build System {(Revised)}} ,author = {Neil Mitchell and Moritz Kiefer and Pepe Iborra and Luke Lau and Zubin Duggal and Hannes Siebenhandl and Javier Neira Sanchez and Matthew Pickering and Alan Zimmerman} ,year = {2020} ,month = {September} ,day = {4} ,booktitle = {Proceedings of the 32nd International Symposium on Implementation and Application of Functional Languages (IFL 2020)} ,location = {University of Kent, UK} ,editor = {Olaf Chitil} ,pages = {1--10} ,url = {https://ndmitchell.com/downloads/paper-building_an_ide_on_top_of_a_build_system_revised-04_sep_2020.pdf} }
Abstract: When developing a Haskell IDE we hit upon an idea - why not base an IDE on an build system? In this paper we'll explain how to go from that idea to a usable IDE, including the difficulties imposed by reusing a build system, and those imposed by technical details specific to Haskell. Our design has been successful, and hopefully provides a blue-print for others writing IDEs.
How to write an IDE (e.g. Ghcide/HLS) starting from a build system (e.g. Shake).
Paper: Building an Integrated Development Environment (IDE) on top of a Build System
Paper, slides, citation, abstract from IFL 2020, with Moritz Kiefer, Pepe Iborra, Luke Lau, Zubin Duggal, Hannes Siebenhandl, Matthew Pickering and Alan Zimmerman, 04 Sep 2020.
@inproceedings{mitchell:ghcide_04_sep_2020 ,title = {Building an Integrated Development Environment {(IDE)} on top of a Build System} ,author = {Neil Mitchell and Moritz Kiefer and Pepe Iborra and Luke Lau and Zubin Duggal and Hannes Siebenhandl and Matthew Pickering and Alan Zimmerman} ,year = {2020} ,month = {September} ,day = {4} ,booktitle = {Draft Proceedings of the 32nd International Symposium on Implementation and Application of Functional Languages (IFL 2020)} ,location = {University of Kent, UK} ,editor = {Olaf Chitil} ,pages = {222--230} ,url = {https://ndmitchell.com/downloads/paper-building_an_ide_on_top_of_a_build_system-04_sep_2020.pdf} }
Abstract: When developing a Haskell IDE we hit upon an idea - why not base an IDE on an build system? In this paper we'll explain how to go from that idea to a usable IDE, including the difficulties imposed by reusing a build system, and those imposed by technical details specific to Haskell. Our design has been successful, and hopefully provides a blue-print for others writing IDEs.
How to write an IDE (e.g. Ghcide) starting from a build system (e.g. Shake).
Paper: Build systems à la carte: Theory and practice
Paper, citation, abstract from Journal of Functional Programing, with Andrey Mokhov and Simon Peyton Jones, 21 Apr 2020.
@inproceedings{mitchell:shake_21_apr_2020 ,title = {Build systems \`a la carte: Theory and practice} ,author = {Andrey Mokhov and Neil Mitchell and Simon Peyton Jones} ,year = {2020} ,month = {April} ,day = {21} ,journal = {Journal of Functional Programming} ,publisher = {Cambridge University Press} ,volume = {30} ,pages = {55} ,doi = {https://doi.org/10.1017/S0956796820000088} ,url = {https://ndmitchell.com/downloads/paper-build_systems_a_la_carte_theory_and_practice-21_apr_2020.pdf} }
Abstract: Build systems are awesome, terrifying – and unloved. They are used by every developer around the world, but are rarely the object of study. In this paper, we offer a systematic, and executable, framework for developing and comparing build systems, viewing them as related points in a landscape rather than as isolated phenomena. By teasing apart existing build systems, we can recombine their components, allowing us to prototype new build systems with desired properties.
Comparing build systems and finding underlying commonalities, a revised version.
Talk: Fixing Records in Haskell
Slides, video, citation, abstract from Haskell eXchange 2019, 11 Oct 2019.
@misc{mitchell:records_11_oct_2019 ,title = {Fixing Records in {Haskell}} ,author = {Neil Mitchell} ,year = {2019} ,month = {October} ,day = {11} ,note = {Presentation from Haskell eXchange 2019} ,url = {https://ndmitchell.com/downloads/slides-fixing_records_in_haskell-11_oct_2019.pdf} }
Abstract: Sadly, Haskell records aren't very good - problems include that field names must be unique and that record updates are not very expressive. A variety of solutions have been proposed over many decades, but none has gained traction. The closest answer Haskell has is the lens library, which famously ups the bar on complexity.
This talk explains how to fix all the pain, and make records a strength of Haskell, without making them harder to use. We show how to encode records and fields in a type class, then use existing Haskell machinery to abstract over multiple field names. This type class has been added to GHC, and is automatically generated for standard Haskell records. Building on that, we provide a convenient syntax through a Haskell preprocessor.
We've validated our design with the DAML programming language (based on the GHC compiler) which uses these records as standard. We're happy to report that users experiences have been very positive.
How to improve Haskell records.
Talk: Making a Haskell IDE
Slides, video, citation, abstract from MuniHac 2019, 07 Sep 2019.
@misc{mitchell:ghcide_07_sep_2019 ,title = {Making a {Haskell} {IDE}} ,author = {Neil Mitchell} ,year = {2019} ,month = {September} ,day = {7} ,note = {Presentation from MuniHac 2019} ,url = {https://ndmitchell.com/downloads/slides-making_a_haskell_ide-07_sep_2019.pdf} }
Abstract: I've always wanted a Haskell IDE. The absence of a simple and robust solution led me to build Ghcid, which I've been using for many years. However, I have moved on, now using a real Haskell IDE based on technology we developed at Digital Asset for the DAML programming language. It turns out building an IDE is harder than I expected, so in this talk I'll cover three topics:
1. The theory behind building an IDE. We use an in-memory dependency graph, with some interesting tweaks.
2. What's there today and how you can use it. I'll also cover the relationship to haskell-ide-engine, DAML and other related projects.
3. What's missing and how you can help. I'll be hacking on the IDE at MuniHac, and everyone is welcome to join in.
Overview of the Ghcide Haskell IDE, including how to use it and the design.
Paper: Build Systems à la Carte
Paper, citation, abstract from ICFP 2018, with Andrey Mokhov and Simon Peyton Jones, 24 Sep 2018.
@inproceedings{mitchell:shake_24_sep_2018 ,title = {Build Systems \`a la Carte} ,author = {Andrey Mokhov and Neil Mitchell and Simon Peyton Jones} ,year = {2018} ,month = {September} ,day = {24} ,journal = {Proceedings ACM Programing Languages} ,volume = {2} ,issn = {2475-1421} ,pages = {79:1--79:29} ,articleno = {79} ,doi = {http://doi.acm.org/10.1145/3236774} ,url = {https://github.com/snowleopard/build/releases/download/icfp-final/build-systems.pdf} }
Abstract: Build systems are awesome, terrifying - and unloved. They are used by every developer around the world, but are rarely the object of study. In this paper we offer a systematic, and executable, framework for developing and comparing build systems, viewing them as related points in landscape rather than as isolated phenomena. By teasing apart existing build systems, we can recombine their components, allowing us to prototype new build systems with desired properties.
Comparing build systems and finding underlying commonalities. This paper won a Distinguished Paper award.
Talk: Distributed Build Systems
Slides, video, citation, abstract from Big Techday 11, 18 May 2018.
@misc{mitchell:shake_18_may_2018 ,title = {Distributed Build Systems} ,author = {Neil Mitchell} ,year = {2018} ,month = {May} ,day = {18} ,note = {Presentation from Big Techday 11} ,url = {https://ndmitchell.com/downloads/slides-distributed_build_systems-18_may_2018.pdf} }
Abstract: Build systems are awesome - but unappreciated. A decade ago I started writing Shake, a Haskell library for implementing build systems, an alternative to Make, but with much more powerful and accurate dependencies. In this talk we trace the origins of Shake, from a small module to build a PhD thesis, to a production quality build system, figuring out the key ideas along the way. By exploring these ideas we see how build systems relate to each other, realise that Excel is really just a build system, and see how Bazel/Buck keep shared caches in the cloud.
Build system comparisons and the engineering inside Shake.
Talk: Deriving Generic Functions by Example (+10 years)
Slides, citation from York Doctoral Symposium 2017, 17 Nov 2017.
@misc{mitchell:derive_17_nov_2017 ,title = {Deriving Generic Functions by Example (+10 years)} ,author = {Neil Mitchell} ,year = {2017} ,month = {November} ,day = {17} ,note = {Presentation from York Doctoral Symposium 2017} ,url = {https://ndmitchell.com/downloads/slides-deriving_generic_functions_by_example-17_nov_2017.pdf} }
An update on Derive and me 10 years after the first YDS.
Talk: Fast XML Parsing with Haskell
Slides, video, citation, abstract from Haskell eXchange 2017, 12 Oct 2017.
@misc{mitchell:hexml_12_oct_2017 ,title = {Fast {XML} Parsing with {Haskell}} ,author = {Neil Mitchell} ,year = {2017} ,month = {October} ,day = {12} ,note = {Presentation from Haskell eXchange 2017} ,url = {https://ndmitchell.com/downloads/slides-fast_xml_parsing_with_haskell-12_oct_2017.pdf} }
Abstract: Haskell has lots of XML parsing libraries, implemented using different techniques, and offering different levels of performance. In this talk, you will learn why, until recently, even the fastest of these libraries was embarrassingly slow compared to state-of-the-art XML parsers. Neil will share how the issue was rectified, with the introduction of the Hexml and Xeno libraries. Hexml uses the Foreign Function Interface (FFI), pushing much of the actual work into C, showing how to move performance sensitive pieces into C and reintegrate them without excessive overhead. In contrast, Xeno is written in pure Haskell, using special development/testing techniques to ensure the optimised code performs comparably to Hexml. You will explore the comparison between these different approaches, and see how they apply beyond just XML parsing.
Comparing FFI with pure Haskell for performance, comparing Hexml to Xeno.
Paper: Isabelle/HOLCF-Prelude
Paper, citation, abstract, with Joachim Breitner, Brian Huffman and Christian Sternagel, 11 Oct 2017.
@inproceedings{mitchell:hlint_11_oct_2017 ,title = {Isabelle/HOLCF-Prelude} ,author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel} ,year = {2017} ,month = {October} ,day = {11} ,url = {https://www.isa-afp.org/browser_info/current/AFP/HOLCF-Prelude/outline.pdf} }
Abstract: The Isabelle/HOLCF-Prelude is a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. We use it to: prove the correctness of the Eratosthenes' Sieve, in its self-referential implementation commonly used to showcase Haskell's laziness; prove correctness of GHC's "fold/build" rule and related rewrite rules, and; certify a number of hints suggested by HLint.
Definitions and proofs for HLint rules in Isabelle.
Talk: Static Analysis of Haskell
Slides, video, citation, abstract from HaskellX Bytes, 11 Jul 2017.
@misc{mitchell:catch_11_jul_2017 ,title = {Static Analysis of {Haskell}} ,author = {Neil Mitchell} ,year = {2017} ,month = {July} ,day = {11} ,note = {Presentation from HaskellX Bytes} ,url = {https://ndmitchell.com/downloads/slides-static_analysis_of_haskell-11_jul_2017.pdf} }
Abstract: Haskell is a strongly typed programming language, which should be well suited to static analysis - specifically any insights about the program which don't require running the program. Alas, while type systems are becoming increasingly powerful, other forms of static analysis aren't advancing as fast. In this talk we'll give an overview of some of the forms of non-type-based static analysis that do exist, from the practical (GHC warnings, HLint, Weeder) to the research (LiquidHaskell, Catch).
A tour of static analysis tools for Haskell, including HLint, Catch and Weeder.
Talk: Drive-by Haskell Contributions
Slides, video, citation from ZuriHac 2017, 09 Jun 2017.
@misc{mitchell:zurihac_09_jun_2017 ,title = {Drive-by {Haskell} Contributions} ,author = {Neil Mitchell} ,year = {2017} ,month = {June} ,day = {9} ,note = {Presentation from ZuriHac 2017} ,url = {https://ndmitchell.com/downloads/slides-drive-by_haskell_contributions-09_jun_2017.pdf} }
How to start contributing to Haskell projects.
Talk: Neil Mitchell on Development Tools
Audio, citation from HaskellCast, 17 Apr 2017.
@misc{mitchell:interview_17_apr_2017 ,title = {Neil Mitchell on Development Tools} ,author = {Neil Mitchell} ,year = {2017} ,month = {April} ,day = {17} ,note = {Presentation from HaskellCast} }
Me being interviewed by Chris Forno and Alp Mestanogullari.
Talk: Shake: Past, Present, Future
Slides, citation, abstract from London Haskell User Group, 26 Oct 2016.
@misc{mitchell:shake_26_oct_2016 ,title = {Shake: Past, Present, Future} ,author = {Neil Mitchell} ,year = {2016} ,month = {October} ,day = {26} ,note = {Presentation from London Haskell User Group} ,url = {https://ndmitchell.com/downloads/slides-shake_past_present_future-26_oct_2016.pdf} }
Abstract: Shake is a Haskell library for implementing build systems, an alternative to Make, but with much more powerful and accurate dependencies. In this talk we trace the origins of Shake, from a small module to build a PhD thesis, to a production quality build system, figuring out the keys ideas along the way. As we look to the future we'll discuss the conversion of the GHC build system to Shake and how Shake can compete against tools like Bazel/Buck from Google/Facebook.
The history and future directions of Shake.
Talk: Plugging Space Leaks, Improving Performance
Slides, video, citation, abstract from Haskell eXchange 2016, 06 Oct 2016.
@misc{mitchell:spaceleak_06_oct_2016 ,title = {Plugging Space Leaks, Improving Performance} ,author = {Neil Mitchell} ,year = {2016} ,month = {October} ,day = {6} ,note = {Presentation from Haskell eXchange 2016} ,url = {https://ndmitchell.com/downloads/slides-plugging_space_leaks_improving_performance-06_oct_2016.pdf} }
Abstract: Confused by foldl' vs foldl? Unsure when you've got the strictness right? Programs taking too much memory and running too slow? You are not alone! Most Haskell programs suffer from "space leaks" - this talk covers examples (all only found and fixed in the last year) from the base library, QuickCheck, pretty, Happy, Alex and Shake. Some fixes saved over 1Gb of memory! Space leaks occur when a program uses more memory than necessary. Haskell, as a lazy language, is particularly vulnerable to a form of space leak where a small accumulator (e.g. an Int) is instead represented by a sequence of updates that grows on each iteration. In this talk, you will learn the gritty details of space leaks, then the session sets off on a quest to remove them from all Haskell programs. You will explore the relationship between space leaks and stack usage, then how to use the existing tools built in to GHC to detect and debug excessive stack usage. These techniques have already slain lots of space leaks, and hopefully in your hands they can destroy even more.
How to detect and fix space leaks.
Paper: Non-recursive Make Considered Harmful - Build Systems at Scale
Paper, citation, abstract from Haskell Symposium 2016, with Andrey Mokhov, Simon Peyton Jones and Simon Marlow, 22 Sep 2016.
@inproceedings{mitchell:shake_22_sep_2016 ,title = {Non-recursive Make Considered Harmful - Build Systems at Scale} ,author = {Andrey Mokhov and Neil Mitchell and Simon Peyton Jones and Simon Marlow} ,year = {2016} ,month = {September} ,day = {22} ,booktitle = {Haskell 2016: Proceedings of the ACM SIGPLAN symposium on Haskell} ,pages = {55--66} ,url = {https://ndmitchell.com/downloads/paper-non_recursive_make_considered_harmful-22_sep_2016.pdf} }
Abstract: Most build systems start small and simple, but over time grow into hairy monsters that few dare to touch. As we demonstrate in this paper, there are a few issues that cause build systems major scalability challenges, and many pervasively used build systems (e.g. Make) do not scale well.
This paper presents a solution to the challenges we identify. We use functional programming to design abstractions for build systems, and implement them on top of the Shake library, which allows us to describe build rules and dependencies. To substantiate our claims, we engineer a new build system for the Glasgow Haskell Compiler. The result is more scalable, faster, and spectacularly more maintainable than its Make-based predecessor.
How to define large build systems using Shake, particularly a new GHC build system.
Talk: Writing Shake Rules
Slides, citation, abstract from London Haskell Hacking Meetup, 16 Aug 2016.
@misc{mitchell:shake_16_aug_2016 ,title = {Writing {Shake} Rules} ,author = {Neil Mitchell} ,year = {2016} ,month = {August} ,day = {16} ,note = {Presentation from London Haskell Hacking Meetup} ,url = {https://ndmitchell.com/downloads/slides-writing_shake_rules-16_aug_2016.pdf} }
Abstract: Shake is a general purpose library for expressing build systems - forms of computation, with caching, dependencies and more besides. Like all the best stuff in Haskell, Shake is generic, with details such as "files" written on top of the generic library. Of course, the real world doesn't just have "files", but specifically has "C files that need to be compiled with gcc". In this hacking session we'll look at how to write Shake rules, what existing functions people have already layered on top of Shake for compiling with specific compilers, and consider which rules are missing. Hopefully by the end we'll have a rule that people can use out-of-the-box for compiling C++ and Haskell.
Designing general purpose custom rules for Shake, targeted towards building C.
Talk: Defining your own build system with Shake
Slides, video, citation, abstract from Haskell eXchange 2015, 09 Oct 2015.
@misc{mitchell:shake_09_oct_2015 ,title = {Defining your own build system with {Shake}} ,author = {Neil Mitchell} ,year = {2015} ,month = {October} ,day = {9} ,note = {Presentation from Haskell eXchange 2015} ,url = {https://ndmitchell.com/downloads/slides-defining_your_own_build_system_with_shake-09_oct_2015.pdf} }
Abstract: Shake, like Make, is a tool for writing build systems. However, unlike Make, Shake features monadic dependencies (your dependencies themselves can depend on the results of previous dependencies), polymorphic dependencies (your dependencies don't have to be files) and stable dependencies (if something rebuilds but doesn't change things that depend on it don't have to rebuild). These features make it much easier to define build systems that have accurate dependencies. Additionally, these features let you define your own custom build system, and then implement a Shake-based interpreter for it. It is often said that the easiest way to solve a problem is to define the perfect language for solving the problem, then write an interpreter. In this talk we'll see how to use Shake to apply that advice to build systems.
How to define your own build system using Shake.
Talk: Shake 'n' Bake
Slides, citation, abstract from Cambridge NonDysFunctional Programmers, 13 Aug 2015.
@misc{mitchell:shake_13_aug_2015 ,title = {Shake 'n' {Bake}} ,author = {Neil Mitchell} ,year = {2015} ,month = {August} ,day = {13} ,note = {Presentation from Cambridge NonDysFunctional Programmers} ,url = {https://ndmitchell.com/downloads/slides-shake_n_bake-13_aug_2015.pdf} }
Abstract: Shake is a Haskell build system, an alternative to Make, but with more powerful and accurate dependencies. I'll cover how to build things with Shake, and why I laugh at non-Monadic build systems (which covers most things that aren't Shake). Shake is an industrial quality library, with a website at http://shakebuild.com.
Bake is a Haskell continuous integration system, an alternative to Travis/Jenkins, but designed for large semi-trusted teams. Bake guarantees that all code arriving in your master branch passes all tests on all platforms, while using as few resources as possible, allowing you to have hours of tests, 100's of commits a day and one a few lonely test servers. Bake is held together with duct tape.
An informal introduction to Shake and Bake.
Talk: Building stuff with Shake
Slides, video, citation, abstract from FP Days 2014, 20 Nov 2014.
@misc{mitchell:shake_20_nov_2014 ,title = {Building stuff with {Shake}} ,author = {Neil Mitchell} ,year = {2014} ,month = {November} ,day = {20} ,note = {Presentation from FP Days 2014} ,url = {https://ndmitchell.com/downloads/slides-building_stuff_with_shake-20_nov_2014.pdf} }
Abstract: Build systems are a key part of any large software project, relied upon by both developers and release processes. It's important that the build system is understandable, reliable and fast.
This talk introduces the Shake build system which is intended to help meet those goals. Users of Shake write a Haskell program which makes heavy use of the Shake library, while still allowing the full power of Haskell to be used.
The Shake library provides powerful dependency features along with useful extras (profiling, debugging, command line handling). This tutorial aims to help you learn how to think about writing build systems, and how to make those thoughts concrete in Shake.
A tutorial on Shake, with lots of standalone examples.
Talk: Gluing things together with Haskell
Slides, video, citation, abstract from Code Mesh 2014, 05 Nov 2014.
@misc{mitchell:shake_05_nov_2014 ,title = {Gluing things together with {Haskell}} ,author = {Neil Mitchell} ,year = {2014} ,month = {November} ,day = {5} ,note = {Presentation from Code Mesh 2014} ,url = {https://ndmitchell.com/downloads/slides-gluing_things_together_with_haskell-5_nov_2014.pdf} }
Abstract: A large software project is more than just the code that goes into a release, in particular you need lots of glue code to put everything together - including build systems, test harnesses, installer generators etc. While the choice of language for the project is often a carefully considered decision, more often than not the glue code consists of shell scripts and Makefiles. But just as functional programming provides a better way to write the project, it also provides a better way to write the glue code. This talk covers some of the technologies and approaches we use at Standard Chartered to glue together the quant library. In particular, we'll focus on the build system where we replaced 10,000 lines of Makefiles with 1,000 lines of Haskell which builds the project twice as fast. We'll also look at how to test programs using Haskell, how to replace ancillary shell scripts with Haskell, and how to use Haskell to generate installers.
A tour of some of my projects designed to glue code together, replacing shell scripts and Makefiles. Covers Shake, NSIS and Bake.
Talk: Colin's Industrial Influence
Slides, citation, abstract from Runifest, 23 Oct 2014.
@misc{mitchell:runcifest_23_oct_2014 ,title = {Colin's Industrial Influence} ,author = {Neil Mitchell} ,year = {2014} ,month = {October} ,day = {23} ,note = {Presentation from Runifest} ,url = {https://ndmitchell.com/downloads/slides-colins_industrial_influence-23_oct_2014.pdf} }
Abstract: Colin has dabbled in many areas of functional programming, from XML processing to data visualisation, from type searching to generic transformations. While most of Colin's contributions have been made from inside a University, their impact has been felt in industry. In this talk we take a whirlwind tour through some of the projects that have influenced us and our work.
A joint talk with Malcolm Wallace covering some projects influenced by Colin Runciman. My slides cover Uniplate and Hoogle.
Paper: Leaking Space - Eliminating memory hogs
Paper, citation, abstract from ACM Queue, 23 Oct 2013.
@article{mitchell:spaceleak_23_oct_2013 ,title = {Leaking Space - Eliminating memory hogs} ,author = {Neil Mitchell} ,year = {2013} ,month = {October} ,day = {23} ,volume = {11} ,issue = {9} ,journal = {ACM Queue} ,url = {https://queue.acm.org/detail.cfm?id=2538488} }
Abstract: A space leak occurs when a computer program uses more memory than necessary. In contrast to memory leaks, where the leaked memory is never released, the memory consumed by a space leak is released, but later than expected. This article presents example space leaks and how to spot and eliminate them.
Overview of what space leaks are and how to eliminate them.
Talk: Everyone should use a generics library!
Slides, video, citation, abstract from Haskell eXchange 2013, 09 Oct 2013.
@misc{mitchell:uniplate_09_oct_2013 ,title = {Everyone should use a generics library!} ,author = {Neil Mitchell} ,year = {2013} ,month = {October} ,day = {9} ,note = {Presentation from Haskell eXchange 2013} ,url = {https://ndmitchell.com/downloads/slides-everyone_should_use_a_generics_library-09_oct_2013} }
Abstract: A generics library allows programmers to express only the interesting part of certain tasks, avoiding lots of boilerplate and making the code significantly shorter and more maintainable. Haskell is awash with excellent generics libraries, including Scrap Your Boilerplate, Generics for the Masses, Generic Deriving and Uniplate, yet many developers will never have used any of them. This talk explains how to use the Uniplate generics library, using examples derived from the Haskell Lint tool (HLint), which makes extensive use of Uniplate.
How HLint was written using Uniplate and why generics libraries matter.
Paper: Certified HLints with Isabelle/HOLCF-Prelude
Paper, citation, abstract from HART 2013, with Joachim Breitner, Brian Huffman and Christian Sternagel, 27 Jun 2013.
@inproceedings{mitchell:hlint_27_jun_2013 ,title = {Certified {HLints} with Isabelle/HOLCF-Prelude} ,author = {Joachim Breitner and Brian Huffman and Neil Mitchell and Christian Sternagel} ,year = {2013} ,month = {June} ,day = {27} ,booktitle = {Haskell And Rewriting Techniques (HART)} ,url = {https://ndmitchell.com/downloads/paper-certified_hlints_with_isabelle_holcf_prelude-27_jun_2013.pdf} }
Abstract: We present the HOLCF-Prelude, a formalization of a large part of Haskell's standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.
Proving some HLint rules with Isabelle/HOLCF.
Paper: Shake Before Building - Replacing Make with Haskell
Paper, slides, video, citation, abstract from ICFP 2012, 10 Sep 2012.
@inproceedings{mitchell:shake_10_sep_2012 ,title = {Shake Before Building - Replacing Make with {Haskell}} ,author = {Neil Mitchell} ,year = {2012} ,month = {September} ,day = {10} ,location = {Copenhagen, Denmark} ,booktitle = {ICFP '12: Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming} ,publisher = {ACM} ,isbn = {978-1-4503-1054-3} ,url = {https://ndmitchell.com/downloads/paper-shake_before_building-10_sep_2012.pdf} }
Abstract: Most complex software projects are compiled using a build tool (e.g. make), which runs commands in an order satisfying user-defined dependencies. Unfortunately, most build tools require all dependencies to be specified before the build starts. This restriction makes many dependency patterns difficult to express, especially those involving files generated at build time. We show how to eliminate this restriction, allowing additional dependencies to be specified while building. We have implemented our ideas in the Haskell library Shake, and have used Shake to write a complex build system which compiles millions of lines of code.
An introduction to Shake, focusing on the theoretical side.
Talk: Hoogle: Finding Functions from Types
Slides, citation from TFP 2011, 16 May 2011.
@misc{mitchell:hoogle_16_may_2011 ,title = {Hoogle: Finding Functions from Types} ,author = {Neil Mitchell} ,year = {2011} ,month = {May} ,day = {16} ,note = {Presentation from TFP 2011} ,url = {https://ndmitchell.com/downloads/slides-hoogle_finding_functions_from_types-16_may_2011.pdf} }
An overview of how type-search works in Hoogle v1 to v4.
Talk: Shake: A Better Make
Slides, video, citation from Haskell Implementors Workshop 2010, 01 Oct 2010.
@misc{mitchell:shake_01_oct_2010 ,title = {Shake: A Better Make} ,author = {Neil Mitchell} ,year = {2010} ,month = {October} ,day = {1} ,note = {Presentation from Haskell Implementors Workshop 2010} ,url = {https://ndmitchell.com/downloads/slides-shake_a_better_make-01_oct_2010.pdf} }
Early details about the design of Shake.
Paper: Rethinking Supercompilation
Paper, slides, video, citation, abstract from ICFP 2010, 29 Sep 2010.
@inproceedings{mitchell:supercompilation_29_sep_2010 ,title = {Rethinking Supercompilation} ,author = {Neil Mitchell} ,year = {2010} ,month = {September} ,day = {29} ,location = {Baltimore, Maryland, USA} ,pages = {309--320} ,booktitle = {ICFP '10: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming} ,doi = {https://doi.acm.org/10.1145/1863543.1863588} ,publisher = {ACM} ,isbn = {978-1-60558-794-3} ,url = {https://ndmitchell.com/downloads/paper-rethinking_supercompilation-29_sep_2010.pdf} }
Abstract: Supercompilation is a program optimisation technique that is particularly effective at eliminating unnecessary overheads. We have designed a new supercompiler, making many novel choices, including different termination criteria and handling of let bindings. The result is a supercompiler that focuses on simplicity, compiles programs quickly and optimises programs well. We have benchmarked our supercompiler, with some programs running more than twice as fast than when compiled with GHC.
Thoughts about making supercompilation faster, based on my experiments with Supero.
Paper: Deriving a Relationship from a Single Example
Paper, slides, citation, abstract from Approaches and Applications of Inductive Programming 2009, 04 Sep 2009.
@inproceedings{mitchell:derive_04_sep_2009 ,title = {Deriving a Relationship from a Single Example} ,author = {Neil Mitchell} ,year = {2009} ,month = {September} ,day = {4} ,location = {Edinburgh, Scotland, UK} ,series = {Lecture Notes in Computer Science, Vol. 5812} ,editors = {Ute Schmid, Emanuel Kitzelmann, Rinus Plasmeijer} ,isbn = {978-3-642-11930-9} ,pages = {1--24} ,url = {https://ndmitchell.com/downloads/paper-deriving_a_relationship_from_a_single_example-04_sep_2009.pdf} }
Abstract: Given an appropriate domain specific language (DSL), it is possible to describe the relationship between Haskell data types and many generic functions, typically type-class instances. While describing the relationship is possible, it is not always an easy task. There is an alternative - simply give one example output for a carefully chosen input, and have the relationship derived.
When deriving a relationship from only one example, it is important that the derived relationship is the intended one. We identify general restrictions on the DSL, and on the provided example, to ensure a level of predictability. We then apply these restrictions in practice, to derive the relationship between Haskell data types and generic functions. We have used our scheme in the Derive tool, where over 60% of type classes are derived from a single example.
Assuming you have a single example of a type class, what should the data type be, and what range of instances can be described. Implemented in the Derive tool.
Paper: Losing Functions without Gaining Data
Paper, slides, video, citation, abstract from Haskell Symposium 2009, with Colin Runciman, 03 Sep 2009.
@inproceedings{mitchell:defunctionalisation_03_sep_2009 ,title = {Losing Functions without Gaining Data} ,author = {Neil Mitchell and Colin Runciman} ,year = {2009} ,month = {September} ,day = {3} ,booktitle = {Haskell '09: Proceedings of the second ACM SIGPLAN symposium on Haskell} ,pages = {49--60} ,location = {Edinburgh, Scotland, UK} ,doi = {https://doi.acm.org/10.1145/1411286.1411293} ,publisher = {ACM} ,isbn = {978-1-60558-508-6} ,url = {https://ndmitchell.com/downloads/paper-losing_functions_without_gaining_data-03_sep_2009.pdf} }
Abstract: We describe a transformation which takes a higher-order program, and produces an equivalent first-order program. Unlike Reynolds-style defunctionalisation, it does not introduce any new data types, and the results are more amenable to subsequent analysis operations. We can use our method to improve the results of existing analysis operations, including strictness analysis, pattern-match safety and termination checking. Our transformation is implemented, and works on a Core language to which Haskell programs can be reduced. Our method cannot always succeed in removing all functional values, but in practice is remarkably successful.
An algorithm for making higher-order programs first-order without introducing new data types (e.g. without doing Reynold's style defunctionalisation). The resulting program may have worse time complexity, but that's fine for certain types of analysis. Implemented as Firstify and used in Catch.
Talk: Supercompilation for Haskell
Slides, citation from Fun in the Afternoon Spring 2009, 03 Mar 2009.
@misc{mitchell:supercompilation_03_mar_2009 ,title = {Supercompilation for {Haskell}} ,author = {Neil Mitchell} ,year = {2009} ,month = {March} ,day = {3} ,note = {Presentation from Fun in the Afternoon Spring 2009} ,url = {https://ndmitchell.com/downloads/slides-supercompilation_for_haskell-03_mar_2009.pdf} }
Details of how to apply supercompilation to Haskell.
Paper: Hoogle Overview
Paper, citation, abstract from The Monad.Reader, 19 Nov 2008.
@article{mitchell:hoogle_19_nov_2008 ,title = {Hoogle Overview} ,author = {Neil Mitchell} ,year = {2008} ,month = {November} ,day = {19} ,journal = {The Monad.Reader} ,number = {12} ,pages = {27--35} ,url = {https://ndmitchell.com/downloads/paper-hoogle_overview-19_nov_2008.pdf} }
Abstract: This article gives an overview of the Hoogle tool. We describe the history of Hoogle, the improvements that have been made this summer, and plans for future features. Finally, we discuss the design guidelines of Hoogle 4 - which may be of interest both to budding Hoogle developers and other Haskell projects. This article does not cover the theoretical background of Hoogle.
An overview of Hoogle, including both the algorithms and code structure.
Paper: Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching
Paper, slides, video, citation, abstract from Haskell Symposium 2008, with Colin Runciman, 25 Sep 2008.
@inproceedings{mitchell:catch_25_sep_2008 ,title = {Not All Patterns, But Enough - an automatic verifier for partial but sufficient pattern matching} ,author = {Neil Mitchell and Colin Runciman} ,year = {2008} ,month = {September} ,day = {25} ,booktitle = {Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell} ,pages = {49--60} ,location = {Victoria, BC, Canada} ,doi = {https://doi.acm.org/10.1145/1411286.1411293} ,publisher = {ACM} ,isbn = {978-1-60558-064-7} ,url = {https://ndmitchell.com/downloads/paper-not_all_patterns_but_enough-25_sep_2008.pdf} }
Abstract: We describe an automated analysis of Haskell 98 programs to check statically that, despite the possible use of partial (or nonexhaustive) pattern matching, no pattern-match failure can occur. Our method is an iterative backward analysis using a novel form of pattern-constraint to represent sets of data values. The analysis is defined for a core first-order language to which Haskell 98 programs are reduced. Our analysis tool has been successfully applied to a range of programs, and our techniques seem to scale well. Throughout the paper, methods are represented much as we have implemented them in practice, again in Haskell.
A static analysis for automatically proving a program will not raise an error at runtime, implemented as Catch. The analysis was able to detect 3 bugs in the HsColour program.
Talk: Hoogle: Fast Type Searching
Slides, audio, citation from AngloHaskell 2008, 09 Aug 2008.
@misc{mitchell:hoogle_09_aug_2008 ,title = {Hoogle: Fast Type Searching} ,author = {Neil Mitchell} ,year = {2008} ,month = {August} ,day = {9} ,note = {Presentation from AngloHaskell 2008} ,url = {https://ndmitchell.com/downloads/slides-hoogle_fast_type_searching-09_aug_2008.pdf} }
An early overview of how both type and text search works in Hoogle.
Thesis: Transformation and Analysis of Functional Programs
Paper, slides, citation, abstract, 04 Jun 2008.
@phdthesis{mitchell:thesis_04_jun_2008 ,title = {Transformation and Analysis of Functional Programs} ,author = {Neil Mitchell} ,year = {2008} ,month = {June} ,day = {4} ,school = {University of York} ,pages = {225} ,url = {https://ndmitchell.com/downloads/paper-transformation_and_analysis_of_functional_programs-4_jun_2008.pdf} }
Abstract: This thesis describes techniques for transforming and analysing functional programs. We operate on a core language, to which Haskell programs can be reduced. We present a range of techniques, all of which have been implemented and evaluated.
We make programs shorter by defining a library which abstracts over common data traversal patterns, removing boilerplate code. This library only supports traversals having value-specific behaviour for one type, allowing a simpler programming model. Our library allows concise expression of traversals with competitive performance.
We make programs faster by applying a variant of supercompilation. As a result of practical experiments, we have identified modifications to the standard supercompilation techniques -- particularly with respect to let bindings and the generalisation technique.
We make programs safer by automatically checking for potential pattern-match errors. We define a transformation that takes a higher-order program and produces an equivalent program with fewer functional values, typically a first-order program. We then define an analysis on a first-order language which checks statically that, despite the possible use of partial (or non-exhaustive) pattern matching, no pattern-match failure can occur.
My PhD thesis, covering a generics library (Uniplate), a supercompiler (Supero), a defunctionalisation algorithm (Firstify) and a pattern-match safety verifier (Catch).
Talk: Instances for Free
Slides, citation from PLASMA, 22 May 2008.
@misc{mitchell:deriving_22_may_2008 ,title = {Instances for Free} ,author = {Neil Mitchell} ,year = {2008} ,month = {May} ,day = {22} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-instances_for_free-22_may_2008.pdf} }
Generating Haskell instances from examples, as found in the Derive tool.
Paper: A Supercompiler for Core Haskell
Paper, citation, abstract from IFL 2007 post proceedings, with Colin Runciman, 01 May 2008.
@inproceedings{mitchell:supero_01_may_2008 ,title = {A Supercompiler for Core {Haskell}} ,author = {Neil Mitchell and Colin Runciman} ,year = {2008} ,month = {May} ,day = {1} ,pages = {147--164} ,booktitle = {IFL 2007} ,editor = {Olaf Chitil et al.} ,series = {LNCS} ,volume = {5083} ,publisher = {Springer-Verlag} ,url = {https://ndmitchell.com/downloads/paper-a_supercompiler_for_core_haskell-01_may_2008.pdf} }
Abstract: Haskell is a functional language, with features such as higher order functions and lazy evaluation, which allow succinct programs. These high-level features present many challenges for optimising compilers. We report practical experiments using novel variants of supercompilation, with special attention to let bindings and the generalisation technique.
An early design of the Supero supercompiler. This paper won the Peter Landin prize for the best paper presented at the symposium that year, as selected by the programme committee.
Talk: Detecting Pattern-Match Failures in Haskell
Slides, citation from The Oxford Centre for Metacomputation, 26 Nov 2007.
@misc{mitchell:catch_26_nov_2007 ,title = {Detecting Pattern-Match Failures in {Haskell}} ,author = {Neil Mitchell} ,year = {2007} ,month = {November} ,day = {26} ,note = {Presentation from The Oxford Centre for Metacomputation} ,url = {https://ndmitchell.com/downloads/slides-detecting_pattern_match_failures_in_haskell-26_nov_2007.pdf} }
Details about Catch, including worked examples.
Paper: Deriving Generic Functions by Example
Paper, slides, citation, abstract from York Doctoral Symposium 2007, 26 Oct 2007.
@inproceedings{mitchell:deriving_26_oct_2007 ,title = {Deriving Generic Functions by Example} ,author = {Neil Mitchell} ,year = {2007} ,month = {October} ,day = {26} ,pages = {55--62} ,publisher = {Tech. Report YCS-2007-421, Dept. of Computer Science, University of York, UK} ,editor = {Jan Tobias M\"{u}hlberg and Juan Ignacio Perna} ,booktitle = {Proceedings of the First York Doctoral Symposium 2007} ,url = {https://ndmitchell.com/downloads/paper-deriving_generic_functions_by_example-26_oct_2007.pdf} }
Abstract: A function is said to be generic if it operates over values of any data type. For example, a generic equality function can test pairs of booleans, integers, lists, trees etc. In most languages programmers must define generic functions multiple times, specialised for each data type. Alternatively, a tool could be used to specify the relationship between the data type and the implementation, but this relationship may be complex. This paper describes a solution: given a single example of the generic function on one data type, we can infer the relationship between a data type and the implementation. We have used our method in the Derive tool, allowing the implementation of 60% of the generic functions to be inferred.
An early version of the generic deriving work from Derive.
Paper: Uniform Boilerplate and List Processing
Paper, slides, video, citation, abstract from Haskell Workshop 2007, with Colin Runciman, 30 Sep 2007.
@inproceedings{mitchell:uniplate_30_sep_2007 ,title = {Uniform Boilerplate and List Processing} ,author = {Neil Mitchell and Colin Runciman} ,year = {2007} ,month = {September} ,day = {30} ,booktitle = {Haskell '07: Proceedings of the ACM SIGPLAN workshop on Haskell} ,pages = {49--60} ,location = {Freiburg, Germany} ,doi = {https://doi.acm.org/10.1145/1291201.1291208} ,publisher = {ACM} ,isbn = {978-1-59593-674-5} ,url = {https://ndmitchell.com/downloads/paper-uniform_boilerplate_and_list_processing-30_sep_2007.pdf} }
Abstract: Generic traversals over recursive data structures are often referred to as boilerplate code. The definitions of functions involving such traversals may repeat very similar patterns, but with variations for different data types and different functionality. Libraries of operations abstracting away boilerplate code typically rely on elaborate types to make operations generic. The motivating observation for this paper is that most traversals have value-specific behaviour for just one type. We present the design of a new library exploiting this assumption. Our library allows concise expression of traversals with competitive performance.
Details of the Uniplate generics library, including information on how to use the Uniplate operations.
Paper: Supero: Making Haskell Faster
Paper, slides, citation, abstract from IFL 2007, with Colin Runciman, 27 Sep 2007.
@inproceedings{mitchell:supercompilation_27_sep_2007 ,title = {Supero: Making {Haskell} Faster} ,author = {Neil Mitchell and Colin Runciman} ,year = {2007} ,month = {September} ,day = {27} ,booktitle = {IFL 2007: Draft Proceedings of the 19th International Symposium on Implementation and Application of Functional Languages} ,location = {Freiburg, Germany} ,publisher = {Tech. Report No. 12-07 of the Computing Laboratory, University of Kent, UK} ,editor = {Olaf Chitil} ,pages = {334--349} ,url = {https://ndmitchell.com/downloads/paper-supero_making_haskell_faster-27_sep_2007.pdf} }
Abstract: Haskell is a functional language, with features such as higher order functions and lazy evaluation, which allow succinct programs. These high-level features are difficult for fast execution, but GHC is a mature and widely used optimising compiler. This paper presents a whole-program approach to optimisation, which produces speed improvements of between 10% and 60% when used with GHC, on eight benchmarks.
A very early version of Supero, before it was an actual supercompiler.
Talk: Faster Haskell
Slides, citation from Anglo Haskell 2007, 10 Aug 2007.
@misc{mitchell:supercompilation_10_aug_2007 ,title = {Faster {Haskell}} ,author = {Neil Mitchell} ,year = {2007} ,month = {August} ,day = {10} ,note = {Presentation from Anglo Haskell 2007} ,url = {https://ndmitchell.com/downloads/slides-faster_haskell-10_aug_2007.pdf} }
Early work on Supercompilation.
Talk: Yhc: Past, Present, Future
Slides, citation from Anglo Haskell 2007, 10 Aug 2007.
@misc{mitchell:yhc_10_aug_2007 ,title = {Yhc: Past, Present, Future} ,author = {Neil Mitchell} ,year = {2007} ,month = {August} ,day = {10} ,note = {Presentation from Anglo Haskell 2007} ,url = {https://ndmitchell.com/downloads/slides-yhc_past_present_future-10_aug_2007.pdf} }
The history behind Yhc, along with future plans and intentions.
Talk: Transformation and Analysis of Haskell Source Code
Slides, citation from my thesis seminar, 02 Jul 2007.
@misc{mitchell:thesis_02_jul_2007 ,title = {Transformation and Analysis of {Haskell} Source Code} ,author = {Neil Mitchell} ,year = {2007} ,month = {July} ,day = {2} ,note = {Presentation from my thesis seminar} ,url = {https://ndmitchell.com/downloads/slides-transformation_and_analysis_of_haskell_source_code-02_jul_2007.pdf} }
Slides giving a very quick overview of my thesis.
Talk: Fastest Lambda First
Slides, citation from PLASMA, 30 May 2007.
@misc{mitchell:supercompilation_30_may_2007 ,title = {Fastest Lambda First} ,author = {Neil Mitchell} ,year = {2007} ,month = {May} ,day = {30} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-fastest_lambda_first-30_may_2007.pdf} }
Details of a whole-program optimiser for Haskell, early work on Supero.
Paper: Yhc.Core - from Haskell to Core
Paper, citation, abstract from The Monad.Reader, with Dimitry Golubovsky and Matthew Naylor, 30 Apr 2007.
@article{mitchell:yhc_30_apr_2007 ,title = {{Yhc.Core} - from {Haskell} to Core} ,author = {Dimitry Golubovsky and Neil Mitchell and Matthew Naylor} ,year = {2007} ,month = {April} ,day = {30} ,journal = {The Monad.Reader} ,number = {7} ,pages = {45--61} ,url = {https://ndmitchell.com/downloads/paper-yhc_core-30_apr_2007.pdf} }
Abstract: The Yhc compiler is a hot-bed of new and interesting ideas. We present Yhc.Core - one of the most popular libraries from Yhc. We describe what we think makes Yhc.Core special, and how people have used it in various projects including an evaluator, and a Javascript code generator.
Information about the Yhc core language, its constructors and semantics.
Talk: First Order Haskell
Slides, citation from BCTCS 2007, 06 Apr 2007.
@misc{mitchell:defunctionalisation_06_apr_2007 ,title = {First Order {Haskell}} ,author = {Neil Mitchell} ,year = {2007} ,month = {April} ,day = {6} ,note = {Presentation from BCTCS 2007} ,url = {https://ndmitchell.com/downloads/slides-first_order_haskell-06_apr_2007.pdf} }
An early version of a mechanism for defunctionalising Haskell programs, which later became Firstify.
Talk: Ada: Generics
Slides, citation from the Algorithms and Data Structures course, 07 Mar 2007.
@misc{mitchell:ada_07_mar_2007 ,title = {Ada: Generics} ,author = {Neil Mitchell} ,year = {2007} ,month = {March} ,day = {7} ,note = {Presentation from the Algorithms and Data Structures course} ,url = {https://ndmitchell.com/downloads/slides-ada_generics-07_mar_2007.pdf} }
First-year lecture notes on generics in Ada.
Paper: A Static Checker for Safe Pattern Matching in Haskell
Paper, citation, abstract from TFP 2005 post proceedings, with Colin Runciman, 01 Feb 2007.
@inproceedings{mitchell:catch_01_feb_2007 ,title = {A Static Checker for Safe Pattern Matching in {Haskell}} ,author = {Neil Mitchell and Colin Runciman} ,year = {2007} ,month = {February} ,day = {1} ,publisher = {Intellect} ,booktitle = {Trends in Functional Programming} ,volume = {6} ,isbn = {978-1-84150-176-5} ,url = {https://ndmitchell.com/downloads/paper-a_static_checker_for_safe_pattern_matching_in_haskell-01_feb_2007.pdf} }
Abstract: A Haskell program may fail at runtime with a pattern-match error if the program has any incomplete (non-exhaustive) patterns in definitions or case alternatives. This paper describes a static checker that allows non-exhaustive patterns to exist, yet ensures that a pattern-match error does not occur. It describes a constraint language that can be used to reason about pattern matches, along with mechanisms to propagate these constraints between program components.
An early version of Catch.
Talk: Playing with Haskell Data
Slides, citation from PLASMA, 18 Jan 2007.
@misc{mitchell:uniplate_18_jan_2007 ,title = {Playing with {Haskell} Data} ,author = {Neil Mitchell} ,year = {2007} ,month = {January} ,day = {18} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-playing_with_haskell_data-18_jan_2007.pdf} }
Generic traversals and transformations over Haskell data types, what would later become Uniplate.
Talk: Haskell With Go Faster Stripes
Slides, citation from PLASMA, 30 Nov 2006.
@misc{mitchell:supercompilation_30_nov_2006 ,title = {Haskell With Go Faster Stripes} ,author = {Neil Mitchell} ,year = {2006} ,month = {November} ,day = {30} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-haskell_with_go_faster_stripes-30_nov_2006.pdf} }
How to make Haskell faster.
Talk: Hat: Windows and WIMP
Slides, citation from Hat Day 2006 (Kent), 05 Oct 2006.
@misc{mitchell:hat_05_oct_2006 ,title = {Hat: {Windows} and {WIMP}} ,author = {Neil Mitchell} ,year = {2006} ,month = {October} ,day = {5} ,note = {Presentation from Hat Day 2006 (Kent)} ,url = {https://ndmitchell.com/downloads/slides-hat_windows_and_wimp-05_oct_2006.pdf} }
Thoughts about how the Hat tools could benefit from GUI elements.
Talk: Catch, A Practical Tool
Slides, citation from BCTCS 2006, 06 Apr 2006.
@misc{mitchell:catch_06_apr_2006 ,title = {Catch, A Practical Tool} ,author = {Neil Mitchell} ,year = {2006} ,month = {April} ,day = {6} ,note = {Presentation from BCTCS 2006} ,url = {https://ndmitchell.com/downloads/slides-catch-06_apr_2006.pdf} }
Very early notes on Catch.
Talk: Catch, Lazy Termination
Slides, citation from PLASMA, 16 Mar 2006.
@misc{mitchell:catch_16_mar_2006 ,title = {Catch, Lazy Termination} ,author = {Neil Mitchell} ,year = {2006} ,month = {March} ,day = {16} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-catch-16_mar_2006.pdf} }
Discussions about what termination means in a lazy language, and how to detect it.
Talk: Hoogle
Slides, citation from PLASMA, 08 Dec 2005.
@misc{mitchell:hoogle_08_dec_2005 ,title = {Hoogle} ,author = {Neil Mitchell} ,year = {2005} ,month = {December} ,day = {8} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-hoogle-08_dec_2005.pdf} }
An early introduction to Hoogle.
Paper: Visual Hat
Paper, slides, citation, abstract from Hat Day 2005 (York), 28 Oct 2005.
@inproceedings{mitchell:hat_28_oct_2005 ,title = {Visual {Hat}} ,author = {Neil Mitchell} ,year = {2005} ,month = {October} ,day = {28} ,booktitle = {Hat Day 2005: work in progress on the Hat tracing system for Haskell} ,pages = {23--26} ,publisher = {Tech. Report YCS-2005-395, Dept. of Computer Science, University of York, UK} ,editor = {Colin Runciman} ,url = {https://ndmitchell.com/downloads/paper-hatday-28_oct_2005.pdf} }
Abstract: This paper describes a new approach to visualizing the data contained in Hat traces. The aim is to cater for Windows users who are more familiar with graphical debugging tools.
Thoughts on how to make the Hat tools work in a GUI.
Paper: Unfailing Haskell: A Static Checker for Pattern Matching
Paper, slides, citation, abstract from TFP 2005, with Colin Runciman, 24 Sep 2005.
@inproceedings{mitchell:catch_24_sep_2005 ,title = {Unfailing {Haskell}: A Static Checker for Pattern Matching} ,author = {Neil Mitchell and Colin Runciman} ,year = {2005} ,month = {September} ,day = {24} ,booktitle = {Proceedings of the Sixth Symposium on Trends in Functional Programming} ,pages = {313--328} ,url = {https://ndmitchell.com/downloads/paper-unfailing_haskell_a_static_checker_for_pattern_matching-24_sep_2005.pdf} }
Abstract: A Haskell program may fail at runtime with a pattern-match error if the program has any incomplete (non-exhaustive) patterns in definitions or case alternatives. This paper describes a static checker that allows non-exhaustive patterns to exist, yet ensures that a pattern-match error does not occur. It describes a constraint language that can be used to reason about pattern matches, along with mechanisms to propagate these constraints between program components.
A very early version of Catch.
Paper: Qualifying Dissertation: Unfailing Haskell
Paper, citation, abstract, 30 Jun 2005.
@misc{mitchell:thesis_30_jun_2005 ,title = {Qualifying Dissertation: Unfailing {Haskell}} ,author = {Neil Mitchell} ,year = {2005} ,month = {June} ,day = {30} ,institution = {University of York} ,url = {https://ndmitchell.com/downloads/paper-qualifying_dissertation-30_jun_2005.pdf} }
Abstract: Programs written in Haskell may fail at runtime with either a pattern match error, or with non-termination. Both of these can be thought of as giving the value $\bot$ as a result. Other forms of failure, for example heap exhaustion, are not considered.
The first section of this document reviews previous work, including total functional programming and sized types. Attention is paid to termination checkers for both Prolog and various functional languages.
The main result from work so far is a static checker for pattern match errors that allows non-exhaustive patterns to exist, yet ensures that a pattern match error does not occur. It includes a constraint language that can be used to reason about pattern matches, along with mechanisms to propagate these constraints between program components.
The proposal deals with future work to be done. It gives an approximate timetable for the design and implementation of a static checker for termination and pattern match errors.
Discussions of total functional programming, an an early prototype of Catch.
Talk: Total Pasta
Slides, citation, abstract from BCTCS 2005, 23 Mar 2005.
@misc{mitchell:total_23_mar_2005 ,title = {Total {Pasta}} ,author = {Neil Mitchell} ,year = {2005} ,month = {March} ,day = {23} ,note = {Presentation from BCTCS 2005} ,url = {https://ndmitchell.com/downloads/slides-total_pasta-23_mar_2005.pdf} }
Abstract: Most errors in computer programs are only found once they are run, which results in critical errors being missed due to inadequate testing. If additional static analysis is performed, then the possibility exists for detecting such errors, and correcting them. This helps to improve the quality of the resulting code, increasing reliability.
In this project the existing static analysis research is reviewed, along with implementations used both by normal programmers, and used in safety critical applications. A static analysis program is then designed and implemented for the experimental pointer based language Pasta.
The resulting program checks for totality, proving that a particular procedure cannot crash and will terminate. Where a procedure does not satisfy this, the preconditions for the procedure are generated.
An algorithm for automatically proving totality of a simple pointer-based programming language.
Talk: Termination checking for a lazy functional language
Slides, citation from my first year literature review seminar, 21 Dec 2004.
@misc{mitchell:termination_21_dec_2004 ,title = {Termination checking for a lazy functional language} ,author = {Neil Mitchell} ,year = {2004} ,month = {December} ,day = {21} ,note = {Presentation from my first year literature review seminar} ,url = {https://ndmitchell.com/downloads/slides-termination_checking_for_a_lazy_functional_language-21_dec_2004.pdf} }
A review of the literature around termination checking, particular in lazy languages.
Talk: A New Parser
Slides, citation from PLASMA, 17 Nov 2004.
@misc{mitchell:parser_17_nov_2004 ,title = {A New Parser} ,author = {Neil Mitchell} ,year = {2004} ,month = {November} ,day = {17} ,note = {Presentation from PLASMA} ,url = {https://ndmitchell.com/downloads/slides-a_new_parser-17_nov_2004.pdf} }
Thoughts about an alternative way to do parsing.
Paper: Total Pasta: Static Analysis For Unfailing Pointer Programs
Paper, citation, abstract, 05 May 2004.
@mastersthesis{mitchell:total_05_may_2004 ,title = {Total {Pasta}: Static Analysis For Unfailing Pointer Programs} ,author = {Neil Mitchell} ,year = {2004} ,month = {May} ,day = {5} ,school = {University of York} ,pages = {86} ,url = {https://ndmitchell.com/downloads/paper-total_pasta_static_analysis_for_unfailing_pointer_programs-05_may_2004.pdf} }
Abstract: Most errors in computer programs are only found once they are run, which results in critical errors being missed due to inadequate testing. If additional static analysis is performed, then the possibility exists for detecting such errors, and correcting them. This helps to improve the quality of the resulting code, increasing reliability.
In this project the existing static analysis research is reviewed, along with implementations used both by normal programmers, and used in safety critical applications. A static analysis program is then designed and implemented for the experimental pointer based language Pasta.
The resulting program checks for totality, proving that a particular procedure cannot crash and will terminate. Where a procedure does not satisfy this, the preconditions for the procedure are generated.
An algorithm for automatically proving totality of a simple pointer-based programming language.