Haskell, as implemented by the Glasgow Haskell Compiler (GHC), allows expressive type-level programming. The most popular type-level programming extension isTypeFamilies, 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 surprisingly subtle. We prove soundness for a simplification of our algorithm, and state and prove a completeness property, though the algorithm is not fully complete. As much of our reasoning surrounds functions defined by a simple pattern-matching structure, we believe our results extend beyond just Haskell. We have implemented our solution on a branch of GHC and plan to make it available to regular users with the next stable release of the compiler.

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.

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 gobeyondconventional dependent type theory in some respects, and have a subtle metatheory.

- Paper: [A4 pdf]

**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.

- Paper: [A4 pdf]

**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.

- Paper: [A4 pdf]

**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'skindsystem with two features promoted from itstypesystem: 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.

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".

- Paper: [A4 pdf]

**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.

- Paper: [A4 pdf]

**Abstract**

Modular languages supportgenerative 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 thenon-parametric featuresof 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.

- Post-publication version with substantial Appendix (PDF) . This Appendix gives a singificantly simplified version of FC, and one that is much closer to what is implemented in GHC. The Appendix also describes coercion optimisation rules.

**Abstract**

We introduce a variant of System F that uses a single mechanism to enable thetype preservingtranslation 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