Physical Sciences and Mathematics Commons^™

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 …