Research Programming Artificial Intelligence Interviews Other

Serokell’s Work on GHC: Dependent Types

Article by Serokell GHC team

September 12th, 2023

6 min read

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.

{-# LANGUAGE RequiredTypeArguments #-}
{-# LANGUAGE ExplicitNamespaces #-}

-- definition site
id' :: forall a -> a -> a
id' (type t) x = x :: t

-- call site
y = id' (type Int) 42

The new type t syntax is guarded behind -XExplicitNamespaces, forall a -> in types of terms is guarded behind -XRequiredTypeArguments.

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:

{-# LANGUAGE RequiredTypeArguments #-}

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

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.

{-# LANGUAGE ScopedTypeVariables #-}
--          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 Proxy?

Next steps:

There are some ideas how to improve it further, but those are low-priority right now.

GHC misc

Fix bug: GHC erroneously rejected ~ or @ as infix operators in Template Haskell splices.
Remove dead code

Previous updates on dependent types

Stay tuned!

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!

tagged:

GHC Haskell

46 upvotes

Get new articles via email

No spam – you'll only receive stuff we’d like to read ourselves.

Serokell’s Work on GHC: Dependent Types