Impact case study database

The above body of research has directly influenced the development of the Glasgow Haskell Compiler (GHC) by providing conceptual clarifications and technical advances showing that dependent types in Haskell were both possible and practical, contradicting the previous consensus which held that an easy-to-use dependently typed Haskell was very unlikely. In 2009, McBride gave a demonstration of SHE at the Haskell Implementer’s Workshop, showing for the first time how simulated dependent types could in principle be added to Haskell [ S1]. Following this, McBride was invited to work with the GHC design team, who were keen to incorporate the features of SHE into GHC. From 2009 to 2013 there then followed regular and direct collaboration between McBride and GHC’s development team to work on GHC's type system features [ S1].

As a result of this collaboration, GHC extended standard Haskell by incorporating four programmer selectable dependent type extensions. This in turn has benefitted programming practice in Haskell by enabling greater functionality, reaching the world-wide Haskell user base. It has also led to positive economic impacts for numerous industrial users of GHC, who have been able to make use of the dependent typing features to produce significantly more reliable software with fewer bugs; as bugs take time and money to fix, this reduces the overall cost of using Haskell.

Incorporating dependent types into the GHC

Collectively, the four extensions informed by McBride’s research form the core of the dependently typed features of GHC, allowing Haskell to function like a native dependently typed language:

• DataKinds (allowing data to be used in types, released February 2012);

• PolyKinds (allowing types to abstract over the datatypes they use, released February 2012);

• ConstraintKinds (simplifying Haskell’s operator overloading by integrating it better with the type system, released February 2012);

• TypeInType (allowing more type dependency, released May 2016).

Citing R1, the paper introducing the implementation of the DataKinds extension notes that: ‘Our design is inspired by Conor McBride’s Strathclyde Haskell Enhancement (SHE) preprocessor’ [ S2a]. The coordination page for the four dependent type extensions to GHC listed above cites Lindley and McBride's Hasochism paper [ R4] as source material providing conceptual clarification on how Haskell's existing feature set can be integrated with dependent types [ S3]. Dependent types are also being incorporated into the Core language of GHC as an ongoing project, using the findings from the ‘Haskell Types with Added Value’ project as a ‘road map’, as stated by a member of the GHC development team in a 2014 keynote conference speech [ S2b]. This keynote speech also referenced R5 as a source of examples for applications of dependent types, noting that many of the examples were transferrable to GHC; the limitations of dependent types in GHC in comparison to Agda, as demonstrated in R5, were discussed as a key motivator for the integration of dependent types in GHC Core language [ S2b]. A new design for GHC with full-spectrum dependent types was published in 2017 and the specification referenced Gundry’s thesis stemming from the project with McBride in multiple places, including the statement that ‘Our design of DC is strongly based on two recent dissertations that combine type equality coercions and irrelevant quantification in dependently-typed core calculi’ [ S2c].

Confirming the role of McBride’s research in these developments, a Senior Principal Researcher at Microsoft Research, who was involved in the ‘Haskell Types with Numeric Constraints’ project and is also a member of the GHC development team, stated:

‘The effort to incorporate dependently typed features into GHC was originally inspired by discussions between myself and McBride, as well as his work on the Strathclyde Haskell Enhancement (SHE)… the project of making Haskell support richer dependent types continues to this day. These additions enable types to more precisely capture program invariants, allowing programmers to build programs that are correct-by-construction, dramatically reducing errors at compile time and hence run time’ [ S1].

Enabling greater functionality in professional programming practice

With dependent types incorporated into the design of GHC Core language, every Haskell programme compiled today using GHC uses McBride’s research. Due to the ubiquity of GHC, it is impossible to state how many programmes have relied on this research implicitly. Nonetheless, explicit use of the GHC extensions directly underpinned by McBride’s research can be identified using Hackage, which, as the main repository of open source Haskell libraries contributed by developers worldwide, provides a strong indication of how Haskell is being used [ S4]. Of the 15,433 packages on Hackage, as of December 2020:

• 998 (6.5%) use the PolyKinds extension.

• 2321 (15.0%) use the DataKinds extension.

• 1568 (10.2%) use the ConstraintKinds extension.

• 227 (1.5%) use the TypeInType extension.

• 3017 (19.5%) use at least one of them [ S4].

That 19.5% of a large repository of open source libraries use relatively new extensions to an established language like Haskell demonstrates the notability of McBride’s contribution to programming practice. Moreover, a number of these users are sizeable companies, including:

GitHub is a Microsoft-owned code hosting platform with over one hundred million code repositories. Semantic, a GitHub tool for code analysis launched in June 2019, is written in Haskell, and its codebase makes substantial use of the DataKinds and ConstraintKinds extensions [ S5]. Semantic is used to enable interactive code navigation via the GitHub web interface [ S5]. This is a deployment of significant scale, reaching millions of users worldwide.

Digital Asset, a US-based financial technology company, developed a smart contract programming language DAML in 2018 and uses the ConstraintKinds extension to simplify the code in their build systems [ S6]. A Senior Product Architect at Digital Asset has stated that ‘ConstraintKinds has been a massive simplification’ having made ‘key signatures 3x simpler, and thus more understandable’ [ S6].

Well-Typed LLP is a UK-based Haskell consultancy, founded in 2008, that is actively using and supporting the use of dependently typed Haskell in client projects [ S7]. Examples since August 2013 include the implementation of a major cryptocurrency, in which dependent types are used as part of a spectrum of verification techniques for higher assurance development, which would not be possible without dependently typed features [ S7].

Facilitating economic benefits for industrial users of Haskell

McBride's work, via GHC, has led to significant economic impacts at a number of major technology companies thanks to improved software correctness and lower development costs.

Habito is a UK-based online mortgage broker. Their online platform has brokered over GBP5,000,000,000 worth of mortgage applications since its founding in 2015, helping over 350,000 people with their home-financing needs [ S8]. Habito is almost exclusively written using GHC Haskell with dependently typed extensions, including all four extensions based on McBride’s research [ S8]. As Habito’s Chief Technologist states: ‘Heavy use of language extensions, particularly those which extend Haskell’s type system, is made throughout the Habito codebase… Over 90% of Habito’s codebase is deployed to production in customer- and institution-facing products many times a week, where it serves many thousands of visitors and customers each day. The majority of engineers interact with this codebase on a daily basis’ [ S8].

By using dependent types in their Haskell code, Habito has been able to save time and lower the risk of introducing logical errors into their programming by reducing the need to validate the same piece of data twice when checking business constraints in their refined library. Dependent types are also used by Habito to generate code that would otherwise have to be written by hand, and to automatically generate audit logs, both of which have saved considerable time for and increased performance for the business. Automatic code generation in particular has been credited as having ‘enabled changes which have increased performance by orders of magnitude, or added completely new back-ends, in relatively short timespans (weeks instead of months)’ [ S8].

Galois is a US-based research and development company. Galois has used dependently typed Haskell to develop its Crucible software, a retargetable software simulator for analysing software written in multiple programming languages, primarily for security and correctness. Crucible makes essential use of dependently typed Haskell to enforce crucial invariants about the systems it is analysing, preventing bugs in the analysis [ S9]. Galois has calculated that Crucible has played an important role in contracts worth over USD22,600,000 (10-2019), demonstrating its significance to the company [ S9]. These include use by Amazon to help ensure security of their ‘s2n’ cryptography library and in several projects funded by the US government on Fully Homomorphic Encryption and Software Brittleness.

As of 2019, US-based technology company Google uses dependently typed Haskell to develop a project to produce a hardware artefact and its supporting software infrastructure that will, in the words of two Senior Software Engineers at Google, be ‘deployed at a huge scale within Google and serve high volume traffic’ [ S10]. This project is being developed with a team of 20 engineers, ‘a large team of engineers (even by Google standards)’ [ S10]. Language extensions that support dependently typed programming in Haskell are used extensively in this project: by January 2019, the codebase contained 15 modules that use the TypeInType extension, 378 modules that use DataKinds, 51 that use PolyKinds and 69 modules that use ConstraintKinds. Highlighting the benefits of these extensions for the project, the Engineers stated:

‘Since we are very much a product group required to develop and deploy sophisticated software in a tight timescale we rely heavily on Haskell’s expressive power as well as the robustness of language extensions for features like dependently typed programming, many of which have been developed at your department [Computer & Information Science, University of Strathclyde]…These language extensions have significantly increased our productivity and helped to find errors early at compile time…Given the tight deadlines we operate to, the extra productivity afforded by the dependently typed programming features developed by Dr McBride et al. has been of great operational importance to us’ [ S10].