Serokell’s Work on GHC: Dependent Types
At Serokell, we have been working hard for some time now to help add dependent types to Haskell. It is the primary goal of our dedicated GHC team, currently consisting of Vladislav Zavialov and Andrei Borzenkov.
We have occasionally shared our progress on Discourse in the past, though in an irregular manner, which has left some wondering if we are still actively working on it. Yes, we are!
However, retrofitting ergonomic dependent types is a very complex task. We want to ensure that new features interact harmoniously with existing ones, and that Haskellers who don’t need dependent types can keep writing Haskell as usual, for example, continue making use of punning.
Haskell is a very rich language, making it infeasible to directly transfer the formalism of other dependently-typed languages. We need to reconcile Dependent Haskell with the GHC constraint solver, deriving mechanism, non-terminating functions and multiplicity polymorphism in linear types.
The aim of this new blog series is to provide regular updates on the work we have done, the obstacles we have encountered, and the breakthroughs we have achieved.
Summary: Two milestones
In the past month, we have achieved two significant milestones, the implementation of part 1 of visible forall and improved name resolution and type checking of type patterns.
Visible forall will allow us to get rid of
AllowAmbiguousTypes and the
Proxy hack. Instead of the clumsy
sizeOf (Proxy :: Proxy Int) it will be possible to write
sizeOf' Int, as types can be required as visible arguments at the definition site and passed as visible arguments at the call site. Even though the more intriguing user-facing changes of this proposal will be implemented in part 2, the heavy lifting, namely the necessary refactoring of GHC, was done in part 1 and is completed.
In a future report, we will explain the close relationship between the new
forall a -> quantifier and pi types, and it will become apparent why visible forall is crucial for adding dependent functions to GHC.
Type patterns has been in the works for a year now, but finding a solution to certain obstacles has proven elusive for a long time. We had to address the fact that the paper, on which the original implementation is based, didn’t discuss kinds. Additionally, we realized that the name resolution part of Modern Scoped Type Variables (#448) was underspecified. As a result, we proposed an amendment (#556) that was accepted and which we have now implemented. This is an important milestone, as the work on visible forall is built upon the foundation provided by this implementation of type patterns.
While working on those issues we also spotted and fixed a bug in Template Haskell and removed some dead code.
Visible forall: Details
Visible forall part 1 introduces the
forall a -> quantifier in types of terms and the
type keyword in term syntax that allows passing types as arguments.
A simple example to illustrate the new syntax is a variation of the identity function that requires the caller to explicitly provide a type argument.
-- definition site id' :: forall a -> a -> a id' (type t) x = x :: t -- call site y = id' (type Int) 42
type t syntax is guarded behind
forall a -> in types of terms is guarded behind
The key aspect of the
forall a -> quantifier is its ability to introduce a parameter that requires the caller to explicitly pass a type as an argument. This has only been possible indirectly using the
Proxy hack. The
type keyword (made optional in part 2) allows passing a type as an argument at the call site (
id' (type Int) 42) and binding that type to a type variable at the definition site (
id' (type t) x = ...).
Note that the new quantifier is an erased quantifier which means that the
a introduced by
forall a -> does not exist at runtime.
This work is merged upstream and planned to land in GHC 9.10.
Next steps: Making it ergonomic
In visible forall part 1, the
type keyword is required to pass and bind a type required by
forall a ->. The goal of part 2 is to make this functionality more ergonomic, so that a type can be passed like any other argument, without additional ceremony.
Once Part 2 is implemented, it will be possible to write
id' like so:
-- definition site id' :: forall a -> a -> a id' t x = x :: t -- No (type x) needed. -- call site y = id' Int 42 -- No @Int, (type Int) or (Proxy :: Proxy Int). -- Int is passed just like any other value.
From a technical standpoint, this means that we need to specify when it is permissible to omit the
type herald. This greatly enhances convenience and this is how it’s done in Agda or Idris, but it also makes the specification more intricate. We already have prototypes of the remaining tickets of #281 (as outlined here Visible forall, Part 2). Our goal for the next few weeks is to finish implementing and merge upstream.
- Proposal text: Visible forall in types of terms, and types in terms, #281
- Discussion: Visible forall in types of terms, and types in terms, #281
- Merged commit: Visible forall in types of terms: Part 1, #22326, commit 33b6850
- Tickets for visible forall, part 2: Visible forall in types of terms, Part 2
- Dependent types proposal: Design for Dependent Types
Type patterns: details
The type patterns changes are primarily internal, but they are still quite impactful as they unblock both part 2 of visible forall and @-binders. GHC didn’t have special logic for type patterns and reused renaming and type checking for pattern signatures, augmented with a few ad-hoc checks. We implemented parsing and renaming logic dedicated specifically to type patterns and fixed the issue with polymorphic kinds in the type-checker.
A user-facing change of this commit is the unification of GHC’s behavior at the term-level and type-level in pattern syntax, which was incoherent for historical reasons. For instance, the shadowing of variables within pattern syntax would result in an error at the type level, whereas it would only issue a warning at the term level.
termVar = 42 -- Brings the term variable 'termVar' into scope. addTen :: Int -> Int addTen termVar = termVar + 10 -- ^^^^^^^ -- WARNING: Shadows 'termVar' that is already in scope.
This code compiles and GHC merely issues a warning that
termVar is already in scope. Now let’s observe how GHC previously reacted when we shadowed a type variable in pattern syntax.
-- Brings the type variable 'tyVar' into scope. -- vvvvv f :: forall tyVar. Proxy tyVar -> [tyVar] f (Proxy @tyVar) =  :: [tyVar] -- ^^^^^^ -- ERROR: Type variable 'tyVar' is alread in scope.
The new implementation unifies the behavior of type-level and term-level and GHC emits a warning in both instances.
By the way, can you see how the last example could be rewritten with visible forall instead of
There are some ideas how to improve it further, but those are low-priority right now.
- Merged commit: Type patterns (#22478, #18986)
- MR waiting to be merged upstream, builds on top of the previous commit: Parser, renamer, type checker for @a-binders (#17594)
- Amendment to #448, discussion: Type arguments in constructor patterns: fix signature scoping #556
- Visibility Orthogonality Principle (VOP)
- Modern Scoped Type Variables (#448), Proposal
- Modern Scoped Type Variables (#448), Discussion
- Fix bug: GHC erroneously rejected
@as infix operators in Template Haskell splices.
- Remove dead code
Previous updates on dependent types
- GHC+DH Weekly Update #1, 2022-12-07 (Discourse)
- GHC+DH Weekly Update #2, 2022-12-21 (Discourse)
- GHC+DH Weekly Update #3, 2023-01-11 (Discourse)
- GHC+DH Weekly Update #4, 2023-01-18 (Discourse)
- GHC+DH Weekly Update #5, 2023-01-25 (Discourse)
- GHC+DH Weekly Update #6, 2023-06-07 (Discourse)
- GHC+DH Weekly Update #7, 2023-06-14 (Discourse)
This was the inaugural blog post of our series “Work on GHC: Dependent Types”. While we won’t have a new post on this every week, we are committed to releasing these updates regularly from now on, so stay tuned!