Research Programming Artificial Intelligence Interviews Other

Serokell’s Work on GHC: Dependent Types, Part 2

Article by Serokell GHC team

December 22nd, 2023

6 min read

At Serokell, we have a dedicated team working on GHC. The primary goal is to help add dependent types to Haskell, as outlined in GHC proposal #378, Design for Dependent Types.

This is a complex undertaking with a wide range of challenging problems. The aim of this blog series is to provide regular updates on the work we have done, the obstacles we have encountered, and the breakthroughs we have achieved.

You can find the previous edition here.

The current GHC team consists of Vladislav Zavialov and Andrei Borzenkov. (As Andrei was engaged in other projects, this report primarily portrays the efforts of Vlad.)

Summary

We have reached another milestone on our journey towards Dependent Haskell: Visible forall, part 2 has been implemented.

This is a crucial step on the path towards ergonomic dependent types in Haskell. The syntax for passing a type as an argument to a function is now as straightforward and concise as in fully dependently-typed languages like Agda.

This almost concludes the implementation of proposal #281, Visible forall in types of terms, and types in terms.

In addition, we wrote an amendment to the visible forall proposal and made efforts to align the ecosystem with the advancements in GHC, e.g. updating documentation and patching libraries.

Visible forall, part 2: Make the type keyword optional

Recap of visible forall, part 1

The major feature of visible forall, part 1 (see last report) was the new ability to require and pass visible type arguments, with the caveat that they had to be prefixed with the new type keyword.

To recall, here’s an example to illustrate the concept. We define show', a modified version of the show function that requires the user to explicitly specify the type of a. That means, it is necessary to pass a type at the term level.

Definition site of show'

{-# LANGUAGE RequiredTypeArguments, ExplicitNamespaces #-}

--    Require user to pass a
--    type as an arg to show'
--       vvvvvvvvvvv
show' :: forall a -> Show a => a -> String  -- New "forall a ->"
show' (type t) x = show (x :: t)            -- New "type" keyword
--    ^^^^^^^^
--    bind type arg to t

Use site of show'

{-# LANGUAGE RequiredTypeArguments, ExplicitNamespaces #-}

--    Pass type Int as an ordinary
--    arg at the term level
--         vvvvvvvvvv
s1 = show' (type Int)    42      -- "42"
s2 = show' (type Double) 42      -- "42.0"
--         ^^^^^^^^^^^^^
--    Pass type Double at
--    the term level

The (type t) syntax is guarded behind -XExplicitNamespaces, the forall a -> quantifier in types of terms is guarded behind -XRequiredTypeArguments.

Goal of visible forall, part 2

Visible forall, part 1 was an important step towards Dependent Haskell, but the syntax was still a bit cumbersome.

In fully dependently-typed languages like Agda, a type can be passed like any other argument, without additional ceremony. The core intention behind visible forall, part 2 was to make the type keyword optional.

This task had two large subtasks.

Make the type keyword optional in expressions, i.e. at use sites, e.g.
f (Maybe Int) instead of the more verbose f (type (Maybe Int)).
Make type optional in patterns, i.e. at binding sites, e.g.
f a x = x :: a instead of f (type a) x = x :: a.

Both subtasks have been implemented, subtask 1 in commit T2T in Expressions and subtask 2 in commits Term variable capture and T2T in Patterns. Part 1 has been merged as of Nov 4.

We can now rewrite the show' function from the example without needing the type keyword.

{-# LANGUAGE RequiredTypeArguments #-}

show' :: forall a -> Show a => a -> String
show' t x = show (x :: t)  -- Bind type to t without type keyword


s1 = show' Int    42       -- Pass type without type keyword
s2 = show' Double 42

Since we no longer need the type keyword, we can also omit -XExplicitNamespaces.

For those who favor the explicit syntax, it remains an option.

`forall` is now a keyword at the term level

Now that we have types at the term level, it has become necessary to make forall a keyword at the term level.

Before this change, forall was a keyword at the type level but an identifier at the term level:

-- Before this change:

id' :: forall -> forall -- Type level: Error. Invalid ty var.
id' x = x

forall = 42             -- Term level: OK, valid identifier.

The Proposed Change Specification of the visible forall proposal makes forall a keyword at both levels, not guarded by any extension. This implies forall is no longer a valid identifier.

forall = 42   -- Parse error. forall is no longer a valid identifier.

Now that -XRequiredTypeArguments allows types like forall a. a -> a in terms, e.g. in

f (forall a. a -> a)

the change was motivated by wanting to avoid situations where the meaning of forall depends on what extensions are enabled.

To address this, we created an issue that is now resolved (relevant commit).

Since this is a breaking change, the warning -Wforall-identifier has been available for three releases (GHC 9.4, 9.6 and 9.8).

Amendment to visible forall proposal

It’s been some time since the visible forall proposal was written. During implementation, it became apparent that it would be beneficial to update some sections of the proposal. This is how amendment #626 came about (Visible forall in types of terms: data constructors, patterns, polytypes, drop the binder restriction).

In this revision we clarify some points that were previously left implicit (e.g. allow forall a -> in data constructors, patterns undergo a term-to-type transformation just like expressions), drop an obsolete restriction and fix an oversight in the typing rules (thanks to Jakob Bruenker for spotting this).

You can read the details here. (Being an amendment, it delves into technical nuances at certain points.)

Haskell ecosystem

While implementing dependent types is a challenging and time-consuming task, our goal is to contribute to keeping the Haskell ecosystem in sync with the evolution of GHC.

With regards to Dependent Haskell, this means updating documentation, doing impact assessment and updating libraries that break due to new DH syntax.

Update GHC User’s Guide

We updated the User’s Guide and Release Notes to account for the recent progress in the implementation of RequiredTypeArguments. You can find the updated section in the User’s Guide here.

Stackage impact assessment

To prepare amendment 626, it was necessary to perform an impact analysis on Stackage.

We modified GHC 9.6 to use the new grammar for view patterns and compiled 3318 packages with the patched compiler.

Patching libraries

Making forall a keyword at the term level was a breaking change. Libraries that use forall as an identifier at the term level will no longer compile.

To avoid placing the burden on maintainers and library authors, we have compiled all packages in head.hackage against the new branch and authored patches where necessary. Moreover, we have compiled popular libraries that do not have patches in head.hackage, but where we suspected they could be affected.

The head.hackage patches are merged upstream.

Previous updates on dependent types

Stay tuned

This was the second blog post of our series “Work on GHC: Dependent Types”. Stay tuned for our updates, which we are committed to releasing regularly!

tagged:

GHC Haskell

17 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, Part 2