Dependent Haskell RoadmapThe Glasgow Haskell Compiler<br>Dependent Types: Current Status

Page structure. This page is an overview of language features and implementation tasks that contribute, directly or indirectly, towards the goal of adding dependent types to Haskell. The tasks are organized into a graph. Edges point to prerequisites or subtasks. Completed tasks are highlighted with a purple border. Accepted proposals awaiting implementation are marked by an orange border. After the graph you will find a grid of cards with information about each node.<br>Target audience. The primary purpose of this page is to track current implementation progress and indicate the relationships between various tasks, thus helping implementors and enthusiasts to see the big picture. You may find it difficult to follow some of the task descriptions if you are new to Haskell or unfamiliar with dependent types, but you might be able to find some useful links and resources.<br>Common questions. Before we proceed to the current state of the project, here are answers to some questions regarding dependent types in the context of Haskell.How are dependent types useful? Just as any other type system feature, dependent types allow the programmer to be more precise about the properties of their code. This has all the usual upsides: less boilerplate, fewer unsafe operations, better correctness guarantees, higher runtime efficiency. For instance, it would be possible to eliminate out-of-bounds array access without the overhead of runtime bounds checking.

How do dependent types fit with existing language features? The existing language extensions (DataKinds, PolyKinds, TypeFamilies, GADTs) allow us to emulate dependent types with techniques such as singleton types and defunctionalized type families. However, the compile-time and run-time costs of these techniques, as well as the associated accidental complexity, limit their applicability. We envision that proper support for dependent types will result in a language that is more well-rounded, easier to learn, and nicer to use.

How do I learn dependent types? At the moment, the best route to understanding dependent types is to learn a language that properly supports them (Agda and Idris are good choices for someone with a Haskell background) and then transfer your understanding back to Haskell. Once we have full support for dependent types in Haskell, it will be possible to create learning resources that do not involve other languages.

Why add dependent types to Haskell? In addition to being a good purely functional programming language, Haskell has a wonderful community, a rich collection of libraries, and high-quality compiler and runtime system. We are lucky to be able to use it in an industrial setting. The initiative to add dependent types to Haskell is motivated by real world use cases. We spotted plentiful opportunities to apply dependent types to improve the quality of our Haskell code.

How long until dependent types are implemented in GHC? We would love to provide an estimate, but it is unclear how long each individual subtask will take. To understand the current state of the project, please consult the task graph below.

Dependent Haskell<br>dependent types in GHC

Dependent retained quantifiers<br>types that refer to terms

Universal promotion<br>promote all terms

Clean up the language<br>preparations for dependent types

Dependent products<br>Π-types

Dependent sums<br>Σ-types

Dependent Core language<br>formalism and implementation

Visible forall<br>in types of terms

Existential quantification<br>first-class exists quantifier

Promote literals<br>numeric, char, string

Promote unboxed types<br>RuntimeRep ≠ LiftedRep

Promote classes<br>constraints and dictionaries

Function promotion<br>promote term-level functions

Data family promotion<br>promote data families

Promote Char<br>and character literals

Promote Natural<br>unify it with Nat

Constrained type families<br>constraints in kinds

Homogeneous equality<br>instead of heterogeneous

Closed term evaluator<br>using bytecode or native code

Open term evaluator<br>normalization by evaluation

Type-level lambdas<br>first-class functions in types

Type-level let-bindings<br>local definitions in types

Type-level case-expressions<br>pattern matching in types

Dependency analysis<br>of top-level declarations

Unsaturated type families<br>partial application in types

Deprecate CUSKs<br>complete user-supplied kinds

Invisible type arguments<br>applications and abstractions

Namespace management<br>to resolve ambiguities

Unify type and kind variables<br>consistent quantification rules

Modifiers syntax<br>generalized modifiers

Standalone kind signatures<br>replacement for CUSKs

Invisible binders in types<br>@k-binders in type declarations

Invisible binders in functions<br>@a-binders in lambdas

Invisible binders in constructors<br>@a-binders in constructor patterns

Visible type applications<br>@t-applications in terms

Visible kind applications<br>@k-applications in types

Syntactic unification<br>type syntax in terms

No star kind...