Physical Sciences and Mathematics Commons^™

The Thoralf Plugin: For Your Fancy Type Needs, Divesh Otwani, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Many fancy types (e.g., generalized algebraic data types, type families) require a type checker plugin. These fancy types have a type index (e.g., type level natural numbers) with an equality relation that is difficult or impossible to represent using GHC’s built-in type equality. The most practical way to represent these equality relations is through a plugin that asserts equality constraints. However, such plugins are difficult to write and reason about. In this paper, we (1) present a formal theory of reasoning about the correctness of type checker plugins for type indices, and, (2) apply this theory in creating Thoralf, a …

Type Variables In Patterns, Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones

Computer Science Faculty Research and Scholarship

For many years, GHC has implemented an extension to Haskell that allows type variables to be bound in type signatures and patterns, and to scope over terms. This extension was never properly specified. We rectify that oversight here. With the formal specification in hand, the otherwise-labyrinthine path toward a design for binding type variables in patterns becomes blindingly clear. We thus extend ScopedTypeVariables to bind type variables explicitly, obviating the Proxy workaround to the dustbin of history.

Extended Abstract: Explaining Type Errors, Brent A. Yorgey, Richard A. Eisenberg, Harley D. Eades Iii

Computer Science Faculty Research and Scholarship

No abstract provided.

Levity Polymorphism, Richard A. Eisenberg, Simon Peyton Jones

Computer Science Faculty Research and Scholarship

Parametric polymorphism is one of the linchpins of modern typed programming, but it comes with a real performance penalty. We describe this penalty; offer a principled way to reason about it (kinds as calling conventions); and propose levity polymorphism. This new form of polymorphism allows abstractions over calling conventions; we detail and verify restrictions that are necessary in order to compile levity-polymorphic functions. Levity polymorphism has created new opportunities in Haskell, including the ability to generalize nearly half of the type classes in GHC's standard library.

Constrained Type Families, J. Garrett Morris, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, modular means of defining type-level computation. However, their current design implicitly assumes that type families are total, introducing nonsensical types and significantly complicating the metatheory of type families and their extensions. We propose an alternative design, using qualified types to pair type-level computations with predicates that capture their domains. Our approach naturally captures the intuitive partiality of type families, simplifying their metatheory. As …

A Specification For Dependent Types In Haskell, Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo De Amorim, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results -- chiefly, type safety, along with theorems that relate these two languages -- have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating …

Levity Polymorphism (Extended Version), Richard A. Eisenberg, Simon Peyton Jones

Computer Science Faculty Research and Scholarship

Parametric polymorphism is one of the lynchpins of modern typed programming. A function that can work seamlessly over a variety of types simplifies code, helps to avoid errors introduced through duplication, and and is easy to maintain. However, polymorphism comes at a very real cost, one that each language with support for polymorphism has paid in different ways. This paper describes this cost, proposes a theoretically simple way to reason about the cost—that kinds, not types, are calling conventions—and details one approach to dealing with polymorphism that works in the context of a language, Haskell, that prizes both efficiency …

Pattern Synonyms, Matthew Pickering, Gergő Érdi, Simon Peyton Jones, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Pattern matching has proven to be a convenient, expressive way of inspecting data. Yet this language feature, in its traditional form, is limited: patterns must be data constructors of concrete data types. No computation or abstraction is allowed. The data type in question must be concrete, with no ability to enforce any invariants. Any change in this data type requires all clients to update their code.

This paper introduces pattern synonyms, which allow programmers to abstract over patterns, painting over all the shortcomings listed above. Pattern synonyms are assigned types, enabling a compiler to check the validity of a …

A Reflection On Types, Simon. Peyton Jones, Stephanie Weirich, Richard A. Eisenberg, Dimitrios Vytiniotis

Computer Science Faculty Research and Scholarship

The ability to perform type tests at runtime blurs the line between statically-typed and dynamically-checked languages. Recent developments in Haskell’s type system allow even programs that use reflection to themselves be statically typed, using a type-indexed runtime representation of types called \𝗍𝖾𝗑𝗍𝗂𝗍{𝖳𝗒𝗉𝖾𝖱𝖾𝗉}\textit{TypeRep}. As a result we can build dynamic types as an ordinary, statically-typed library, on top of \𝗍𝖾𝗑𝗍𝗂𝗍{𝖳𝗒𝗉𝖾𝖱𝖾𝗉}\textit{TypeRep} in an open-world context.

Visible Type Application, Richard A. Eisenberg, Stephanie Weirich, Hamidhasan G. Ahmed

Computer Science Faculty Research and Scholarship

The Hindley-Milner HM type system automatically infers the types at which polymorphic functions are used. In HM, the inferred types are unambiguous, and every expression has a principal type. Type annotations make HM compatible with extensions where complete type inference is impossible, such as higher-rank polymorphism and type-level functions. However, programmers cannot use annotations to explicitly provide type arguments to polymorphic functions, as HM requires type instantiations to be inferred.

We describe an extension to HM that allows visible type application. Our extension requires a novel type inference algorithm, yet its declarative presentation is a simple extension to HM. We …

Safe Zero-Cost Coercions For Haskell, Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

Dependent Types In Haskell: Theory And Practice, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Haskell, as implemented in the Glasgow Haskell Compiler (GHC), has been adding new type-level programming features for some time. Many of these features—generalized algebraic datatypes (GADTs), type families, kind polymorphism, and promoted datatypes—have brought Haskell to the doorstep of dependent types. Many dependently typed programs can even currently be encoded, but often the constructions are painful.

In this dissertation, I describe Dependent Haskell, which supports full dependent types via a backward-compatible extension to today’s Haskell. An important contribution of this work is an implementation, in GHC, of a portion of Dependent Haskell, with the rest to follow. The features I …

Injective Type Families For Haskell, Jan Stolarek, Simon Peyton Jones, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular type- level programming extension is TypeFamilies, which allows users to write functions on types. Yet, using type functions can cripple type inference in certain situations. In particular, lack of injectivity in type functions means that GHC can never infer an instantiation of a type variable appearing only under type functions. In this paper, we describe a small modification to GHC that allows type functions to be annotated as injective. GHC naturally must check validity of the injectivity annotations. The algorithm to do so is …

Safe Zero-Cost Coercions For Haskell, Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

Closed Type Families With Overlapping Equations, Richard A. Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Open, type-level functions are a recent innovation in Haskell that move Haskell towards the expressiveness of dependent types, while retaining the look and feel of a practical programming language. This paper shows how to increase expressiveness still further, by adding closed type functions whose equations may overlap, and may have non-linear patterns over an open type universe. Although practically useful and simple to implement, these features go be- yond conventional dependent type theory in some respects, and have a subtle metatheory.

Experience Report: Type-Checking Polymorphic Units For Astrophysics Research In Haskell, Takayuki Muranushi, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

Many of the bugs in scientific programs have their roots in mistreatment of physical dimensions, via erroneous expressions in the quantity calculus. Now that the type system in the Glasgow Haskell Compiler is rich enough to support type-level integers and other promoted datatypes, we can type-check the quantity calculus in Haskell. In addition to basic dimension-aware arithmetic and unit conversions, our units library features an extensible system of dimensions and units, a notion of dimensions apart from that of units, and unit polymorphism designed to describe the laws of physics. We demonstrate the utility of units by writing an astrophysics …

Ironclad C++ A Library-Augmented Type-Safe Subset Of C++, Christian Delozier, Richard A. Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M.K. Martin, Steve Zdancewic

Computer Science Faculty Research and Scholarship

The C++ programming language remains widely used, de- spite inheriting many unsafe features from C—features that often lead to failures of type or memory safety that manifest as buffer overflows, use-after-free vulnerabilities, or abstrac- tion violations. Malicious attackers can exploit such viola- tions to compromise application and system security.

This paper introduces Ironclad C++, an approach to bringing the benefits of type and memory safety to C++. Ironclad C++ is, in essence, a library-augmented, type-safe subset of C++. All Ironclad C++ programs are valid C++ programs that can be compiled using standard, off-the-shelf C++ compilers. However, not all valid C++ …

System Fc With Explicit Kind Equality, Stephanie Weirich, Justin Hsu, Richard A. Eisenberg

Computer Science Faculty Research and Scholarship

System FC, the core language of the Glasgow Haskell Compiler, is an explicitly-typed variant of System F with first-class type equality proofs called coercions. This extensible proof system forms the foundation for type system extensions such as type families (type- level functions) and Generalized Algebraic Datatypes (GADTs). Such features, in conjunction with kind polymorphism and datatype promotion, support expressive compile-time reasoning.

However, the core language lacks explicit kind equality proofs. As a result, type-level computation does not have access to kind- level functions or promoted GADTs, the type-level analogues to expression-level features that have been so useful. In this paper, …

Dependently Typed Programming With Singletons, Richard A. Eisenberg, Stephanie Weirich

Computer Science Faculty Research and Scholarship

Haskell programmers have been experimenting with dependent types for at least a decade, using clever encodings that push the limits of the Haskell type system. However, the cleverness of these encodings is also their main drawback. Although the ideas are in- spired by dependently typed programs, the code looks significantly different. As a result, GHC implementors have responded with ex- tensions to Haskell’s type system, such as GADTs, type families, and datatype promotion. However, there remains a significant dif- ference between programming in Haskell and in full-spectrum de- pendently typed languages. Haskell enforces a phase separation be- tween runtime values …