History of DH (Dependent Types in Haskell) contributions

Announcements
26

the web of work says :
Last updated: 2025-02-26

Does the web of work need updating, or did the progress you mention happen early last year or earlier?

1 Like
27

Yes, it needs updating.

1 Like
28

You can also mark modifiers syntax (!14781) as implemented!

3 Likes
29

I just had a discussion with Conor McBride:

Would this be an easier small step in the roadmap that already has a large payoff?

Apparently, @adamgundry has worked on this?

7 Likes
30

To fit the diagram on screen I had to make an unfortunate layout choice: some arrows point up and others down. Read with the arrow directions in mind, the roadmap already presents Π-types as something that can happen independently of the other improvements.

Specifically, the “Dependent products” node has two dependencies:

  • Visible forall, which is already implemented by yours truly.
  • Dependent Core language, which means adding Π-types and dependent pattern matching to Core.

That’s it. There’s no claim that we’d have to, in Conor’s words, “pump the entire Haskell term language up to the type level.”

So, as far as low-hanging fruit is concerned, the next steps could be:

  1. add foreach and dcase to Core
  2. add foreach to the surface language; for case analysis, we’d probably want to overload the usual case syntax and choose between Core-level case and dcase in the desugarer

Nothing else on the roadmap is a blocker.

Of course, whether adding something to Core counts as “low-hanging fruit” or a “small step” is debatable. We’re talking about a new type form (foreach) and a new term form (dcase).

And yes, Adam’s thesis “Type Inference, Haskell and Dependent Types” is fantastic.

11 Likes
31

Do I understand correctly that the main hindrance for dependent core is that that’s a huge bureaucratic effort? Or are there any theoretical hurdles?

1 Like
32

Ah, so that means the dependency arrows are not necessarily transitive. Because that doesn’t depend on type level lambdas, let, case, and the open term evaluator. That is a bit confusing.

Edit: ah, those arrows are going from bottom to top.

33

The arrows are transitive, but note the arrowheads and read A -> B as “A depends on B”.

1 Like
34

There’s more than one way to get to a Dependent Core. Various formalisms are presented in:

I’m going to update the roadmap with these links.

The main theoretical questions are:

  1. Whether to combine the term and type languages within Core (the ambitious vs. the incremental approach).
  2. How to combine dependent types with linear types (don’t forget multiplicity polymorphism).

Long-term, I’d prefer a Core that combines the term and type languages. But realistically, if the goal is to get to Π-types via the safest route without reengineering half of GHC, Adam’s thesis presents a compelling phase-separated approach.

Hmm. This conversation has proved rather insightful. I think I now realise what Conor was hinting at. Indeed, we could start with a Core that simply adds foreach and dcase, then work on combining terms and types afterwards.

10 Likes
35

Hmm. This conversation has proved rather insightful. I think I now realise what Conor was hinting at. Indeed, we could start with a Core that simply adds foreach and dcase, then work on combining terms and types afterwards.

Interesting. Maybe (no rush) you could spell out what (precisely) Core would look like with these extensions.

And before we get to extending Core, it’d be good to get to a stable fixpoint where we have fleshed out all the corners of DH-without-foreach. You are busy doing that (required type arguments etc etc), which is fantastic. But I don’t have a clear idea of what remains to be done. One thing is

  • Combine HsType and HsExpr

But there is probably more. Where’s the canonical place to look?

Thanks for your patient and careful work on this long project!

11 Likes
36

From the sidelines: ditto, and I’m very much enjoying RequiredTypeArguments!

9 Likes
37

Yes, we’d certainly have to put together a GHC proposal, if not a paper as well. I know changes to Core are not taken lightly. Before that happens, it would also be great to bring the existing GHC Core Spec up to date. It lags somewhat behind the implementation.

For the bird’s-eye view, there’s the “Dependent Haskell Roadmap”, which this thread is about. Two things I’d highlight:

  • The most promising next major feature on that roadmap is Unsaturated Type Families, which are now unblocked thanks to @philh’s recent work on Modifiers.
  • On the language cleanup front, I’m grateful to @jaror for resuscitating the work on Pun Warnings in #765.

Closer to the ground, the next batch of issues is on the wiki page “DH Current Status”. It’s a bit out of date, but not terribly so.

9 Likes
38
  • Adding foreach requires a change to Type, but that seems to be less controversial as required type arguments also needed to change that.
  • And dcase is just a case expression where every constructor gets an extra evidence argument which does not actually require changing the Expr type at all (only how it is used). Perhaps we could add a Bool flag (like we did for join points) to make it clearer when it is a dependent match.
  • I’m not sure if we need to add new coercion forms.

So maybe this is not a very large change at all?

2 Likes
39

As I noted in the other thread Which extensions should be part of the next GHC20xx? - #43 by jaror, I think we should also start a GHC proposal to change the naming rules at the type level. In a future with a unified namespace this will need to be the same as the term level. Specifically:

  • type family names must start with lowercase letter
  • infix data type names must start with :, just like operators on the term level, for example: data (:+:) a b = L a | R b.
  • type variables are allowed to be infix names, for example forall (~>). Int ~> Int (the function arrow -> is still reserved)

Maybe more?

2 Likes
40

type family names must start with lowercase letter

In a world where type families are central to DH, I think that’s a good idea. But is that the goal? My ideal future is one where DH allows us to freely mix types/terms in functions, hence there is no need for -XTypeFamilies to write type level functions.

E.g. instead of

type Foo :: Type -> Type
type family Foo a where
  Foo Int = Char
  Foo String = Bool

bar :: forall a. a -> Foo a

we have

foo :: Type -> Type
foo Int = Char
foo String = Bol

bar :: forall a. a -> foo a

In this world, -XTypeFamilies would hopefully be legacy.

5 Likes
41

There are still open type families, which can’t be subsumed by functions. I guess the idea is to allow type classes to be promoted too?

42

Current type families can produce “evidence” of type equality (which I think it means “coercions” at the Core level). Would functions used at the type level in a future DH work in a similar way?

43

It’s not the end goal, but it is one of the intermediate steps. It will probably still take a few years until you can promote functions, so until then I think it would be nice to bring type families more into line with future promoted functions.

Can you elaborate on this, perhaps with an example?

1 Like
44

I’m not very knowledgeable in the workings of type families myself, but consider this example:

{-# LANGUAGE 
        GHC2024, 
        TypeFamilies, 
        FunctionalDependencies, 
        UndecidableInstances,
        RequiredTypeArguments, TypeAbstractions,
        TypeData #-}

import Data.Proxy

type data Nat = Z | S Nat

type family Add (n :: Nat) (m :: Nat) :: Nat where
  Add Z     m = m
  Add (S n) m = S (Add n m)

-- the fundep formulation of the type family above
class AddC (n :: Nat) (m :: Nat) (r :: Nat) | n m -> r
instance AddC Z m m
instance AddC n m r => AddC (S n) m (S r)

works :: forall n m -> forall r r'. (Add n m ~ r, Add n m ~ r') => Proxy r'
works _ _ @r = Proxy @r

-- This doesn't compile, r and r' can't be matched
-- doesnt :: forall n m -> forall r r'. (AddC n m r, AddC n m r') => Proxy r'
-- doesnt _ _ @r = Proxy @r

Even as the fundep in AddC ensures that r and r' will be the same type, GHC can’t work with that knowledge in the doesnt function. But with the type family it works.

45

Here you’re adding equality constraints manually. This also works without any type families involved:

works :: forall n m -> forall r r' x. (x ~ r, x ~ r') => Proxy r'
works _ _ @r = Proxy @r
2 Likes