Safe coercions

Safe coercions, Joachin Breitner, Richard Eisenberg, Simon Peyton Jones, and Stephanie Weirich. Submitted to ICFP 2014. Abstract
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 into GHC.

Closed type families with overlapping equations

Closed type families with overlapping equations, Richard Eisenberg, Dimitrios Vytiniotis, Simon Peyton Jones, and Stephanie Weirich. POPL 2014. Abstract
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 beyond conventional dependent type theory in some respects, and have a subtle metatheory.

Evidence normalization in System FC

Evidence normalization in System FC, Dimitrios Vytiniotis and Simon Peyton Jones. 24th International Conference on Rewriting Techniques and Applications (RTA'13) Eindhoven, June 2013.

Abstract

System FC is an explicitly typed language that serves as the target language for Haskell source programs. System FC is based on System F with the addition of erasable but explicit type equality proof witnesses. Equality proof witnesses are generated from type inference performed on source Haskell programs. Such witnesses may be very large objects, which causes performance degradation in later stages of compilation, and makes it hard to debug the results of type inference and subsequent program transformations. In this paper we present an equality proof simplification algorithm, implemented in GHC, which greatly reduces the size of the target System FC programs.

Equality proof and deferred type errors

Equality proof and deferred type errors, Dimitrios Vytiniotis, Simon Peyton Jones, and Jose Pedro Magalhaes. ICFP'12

Abstract

The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates first-class equality proofs in its intermediate language. We describe a simple, elegant technique that exploits these equality proofs to support \emph{deferred type errors}. The technique requires us to treat equality proofs as possibly-divergent terms; we show how to do so without losing either soundness or the zero-overhead cost model that the programmer expects.

Giving Haskell a promotion

Giving Haskell a promotion, Brent Yorgey, Stephanie Weirich, Julien Cretin, Simon Peyton Jones, adn Dimitrios Vytiniotis, ACM Workshop on Types in Languages Design and Implementation, TLDI'12, Philadelphia, Jan 2012.

Abstract

Static type systems strive to be richly expressive while still being simple enough for programmers to use. We describe an experiment that enriches Haskell's kind system with two features promoted from its type system: data types and polymorphism. The new system has a very good power-to-weight ratio: it offers a significant improvement in expressiveness, but, by re-using concepts that programmers are already familiar with, the system is easy to understand and implement.

Practical aspects of evidence-based compilation in System FC

Practical aspects of evidence-based compilation in System FC, Dimitrios Vytiniotis and Simon Peyton Jones, Rejected by ICFP 2011.

This paper was completely rewritten and reborn as two separate papers, both above: (a) "Equality proofs and deferred type errors" and (b) "Evidence normalization in System FC".

Abstract

System FC is an explicitly typed language that serves as the target language for Haskell source programs. System FC is based on System F with the addition of erasable but explicit type equality proof witnesses. This paper improves FC in two directions: The first contribution is extending term-level functions with the ability to return equality proof witnesses, which allows the smooth integration of equality superclasses and indexed constraint synonyms, features currently absent from Haskell. We show how to ensure soundness and satisfy the zero-cost requirement for equality witnesses using a familiar mechanism, already present in GHC: that of unlifted types. Our second contribution is an equality proof simplification algorithm, which greatly reduces the size of the target System FC terms.

Generative Type Abstraction and Type-level Computation

Generative Type Abstraction and Type-level Computation, Stephanie Wirich, Dimitrios Vytiniotis, Simon Peyton Jones, and Steve Zdancewic, POPL 2011.

Abstract

Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of newer type systems, such as indexed type families and GADTs. In this paper we solve the problem by using kinds to distinguish between parametric and non-parametric contexts. The result is directly applicable to Haskell, which is rapidly developing support for type-level computation, but the same issues should arise whenever generativity and non-parametric features are combined.

System F with Type Equality Coercions

System F with Type Equality Coercions, Martin Sulzmann, Manuel Chakravarty, and Simon Peyton Jones. Proc ACM Workshop on Types in Language Design and Implementaion (TLDI'07), Nice, Jan 2007.

Abstract

We introduce a variant of System F that uses a single mechanism to enable the type preserving translation of generalised abstract data types (GADTs), type classes with associated types and functional dependencies, as well as closed type functions. The core idea is to pass around explicit evidence for type equalities, just like System F passes types explicitly. We use this evidence to justify type casts encoding non-syntactic type equalities induced by the mentioned source language features. In particular, we don't need special typing rules for pattern matching on GADTs, we can easily combine GADTs with type classes, and we can relax restrictions on programs involving associated types or functional dependencies.

Simon Peyton Jones, simonpj@microsoft.com