[Serokell Blog] Work on GHC: Dependent Types, Part 3

Links
#1

Hi all. It’s about time that our GHC team at Serokell published another report, so here we go, I wrote one. You can read it here: Dependent types in Haskell, Part 3

39 Likes
#2

Great work Andrei and Vlad. Thank you!

Simon

5 Likes
#3

I must say that, not even from a Dependent Haskell aspect, these changes just feel really nice in general. They feel like quality of life updates to just be able to be specific on all levels :+1:
I’m definitely looking forward to GHC 9.10 and beyond now :smiley:

4 Likes
#4

This is so nice, really appreciate the work! <3

2 Likes
#5

Thanks for the update and great work! It will be interesting to see how these new extensions affect the current state of the syntax highlighter. With visible dependent quantification it may not be so simple now to tell what arguments are constructors and what arguments are types!

#6

You are contrasting “constructors” and “types”, but it’s not clear to me what you mean by that. This is not a dichotomy I’m aware of, e.g. Int is a type constructor, so it is a type and a constructor at the same time.

It’s not that I want to nitpick terminology. The terminology is a bit messy anyway (people tend to use the words “type” and “constructor” even for things that are neither types nor constructors, e.g. type families). However, I want to address your concern about syntax highlighting and to do that, I need to understand what problem you have in mind. Could you perhaps demonstrate it with examples?

1 Like
#7

In this Report, the unqualified term “constructor” always means “data constructor”.
[Haskell 2010 Report §4.2.1]

Is that no longer a reasonable convention with Dependent Types? I took @mixphix to be asking about constructors-as-“data constructors”.

I guess a datatype promoted to a kind gives data constructors that are also type constructors. It’d still be helpful for the syntax highlighter to be able to tell which syntactic context is using that constructor for which purpose. Oh, except with DT we can now put types in expressions without necessarily the type herald.

#8

So at the moment, types in expressions are clearly syntactically signalled by appearing either to the right of :: or after @. With sufficient dependent types work this starts to blur.

That means that you can’t, for example, reliably syntax highlight a type variable differently from a term variable.

The only real solution to this is semantic highlighting, which I think is popular in dependently typed languages partly for this reason. Fortunately, HLS now supports semantic highlighting, so that should mitigate some of the problems.

1 Like
#9

Saying “constructor” to mean “data constructor” is still a reasonable shorthand when the meaning is clear from context. I’m just asking for additional clarity. Let’s assume that we are contrasting data constructors and type constructors. In that case, I believe that properly supporting RequiredTypeArguments in a syntax highlighter would only require as much machinery as supporting DataKinds. With DataKinds, say we have a type signature of the following form:

f :: Proxy X -> ...

Now, is X a data constructor or a type constructor? This depends on how it was declared:

  • data X = A | B | C -- X is a type constructor
  • data T = X | Y | Z -- X is a data constructor

And the declaration could be in another module. So already we have a situation where highlighting type constructors and data constructors requires module-aware name resolution, something that most syntax highlighters don’t even attempt.

The situation with RequiredTypeArguments is analogous. Say we have a function call f X, is the X a type constructor or a data constructor? We need to do name resolution to figure this out.

Yes, it’s a challenge, but it’s not a new challenge by any means.

I guess a datatype promoted to a kind gives data constructors that are also type constructors.

I see where you’re coming from, but I would like to draw a distinction between “types” and “type-level data”. Types are possibly inhabited, so their kind ends in Type, e.g. Int :: Type or Maybe :: Type -> Type. This means that it’s valid to say x :: Int or m :: Maybe a. With DataKinds, we have type-level data, e.g. True :: Bool could be promoted and used at the type level, but I’d still consider True a data constructor because it does not construct a type, as it is an error to say b :: True, this is simply ill-kinded. So we typically talk about

  • type constructors (kind ends in Type, or more generally TYPE r)
  • class constructors (kind ends in Constraint)
  • data constructors (type/kind ends in a data type, e.g. Bool or Maybe a)

And for convenience, type and class constructors are often lumped together, so “type constructor” often means “type or class constructor”. Admittedly, this makes the terminology not very precise, but I still can say with certainty that True is always a data constructor, never a type constructor, even if promoted.

Yes, variables are way more interesting in this regard. With constructors, you only need name resolution to determine whether it’s a data constructor or a type constructor. It is apparent from the declaration of the said constructor. But for a variable, you actually need to know the type signature to determine if it’s a term variable or a type variable.

f :: Bool -> ...
g :: forall (b :: Bool) -> ...
f x = ...
g x = ...

The equations for f and g are similar, but the x in f is a term variable, while the x in g is a type variable. This time the distinction isn’t “type/class/data” but “type/term”, so the primary distinguishing characteristic is erasure. Different syntax highlighting for erased/retained variables indeed requires type-aware semantic highlighting.

Perhaps I could rephrase the concern expressed in the original comment as follows:

With visible dependent quantification it may not be so simple now to tell what arguments are constructors retained and what arguments are types erased!

3 Likes