Programming Languages and Compilers Commons^™

A Survey Of Practical Haskell: Parsing, Interpreting, And Testing, Parker Landon

Honors Projects

Strongly typed pure functional programming languages like Haskell have historically been confined to academia as vehicles for programming language research. While features of functional programming have greatly influenced mainstream programming languages, the imperative programming style remains pervasive in practical software development. This paper illustrates the practical utility of Haskell and pure functional programming by exploring “hson,” a scripting language for processing JSON developed in Haskell. After introducing the relevant features of Haskell to the unfamiliar reader, this paper reveals how hson leverages functional programming to implement parsing, interpreting, and testing. By showcasing how Haskell’s language features enable the creation of …

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.

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 …

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 …

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 …

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.

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 …

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 …