[ghc-steering-committee] Proposal: Define Kinds Without Promotion (#106)

[Richard Eisenberg]

> On Aug 15, 2018, at 9:41 AM, Eric Seidel <eric at seidel.io> wrote:
> 
> The normal syntax for exporting data constructors would export the constructor in both the value namespace AND the type namespace. But we didn't want the constructor in the value namespace to begin with. I think this is the issue, we have no way to export ONLY the constructor in the type namespace.

I disagree here. The normal syntax exports data constructors only in the data-level namespace, because those constructors don't live at all in the type-level namespace. (The ' syntax doesn't promote anything: it's just a signal to the renamer to look only in the data-level namespace, bypassing the normal type-level lookup.) Right now, the only way to get a data constructor in the type-level namespace is to use a type synonym, and (presumably) the author of this proposal finds that fact annoying (understandably).

> 
> I think "type-level data constructors" just makes things more confusing. The way I think about it (and I could certainly be wrong!), data constructors produce objects that can be used at the value level, and type constructors produce objects that can be used at the type level.

This is a common usage of these terms, so you're not alone. But I don't think it's a helpful vocabulary. The dependent types literature diverges from this usage considerably, not distinguishing between runtime data and compile-time data. As GHC inches toward dependent types (even if we get no further in this direction, the "promotion" feature is directly inspired by dependent types), I think updating our usage of these vocabulary words will be helpful.

> We still have a value/type level distinction in Haskell, so the term "type-level data constructor" reads like an oxymoron to me.

Is it perhaps more comfortable to think of compile-time data vs. runtime data?

> Another way of saying this could just be that "data" constructors live in the value namespace, while "type" constructors live in the type namespace.

I think it all boils down to vocabulary here. We could define the terms this way. But then we need to talk about promoting data constructors to type constructors. We also have the awkwardness of explaining that, say, `'True` is a type (it is used on the type level) but no values have type `'True`. I think it's much clearer to say that `'True` is type-level data. No promotion anymore, just namespaces, and we reserve type to mean things like `Int`.
> 
> If you think of type constructors in my sense, then I think it also makes sense to call the constructors introduced by `type data` type constructors. 

Agreed about this implication. But since I don't satisfy your premise, I'm not bound to agree with your conclusion.

To be clear, I don't think there's a "right" vocabulary and a "wrong" vocabulary here. (And perhaps my email from yesterday is too strongly worded in places around this -- apologies.) I do think the vocabulary I'm advocating for will lead to a simpler formulation of this all and will help Haskellers get a better intuition around these features than the other vocabulary. This change has been slow to formulate in my own head, and is the result of thinking about these issues a lot over the past years -- I, too, have wanted to call data constructors used in types "type constructors". I no longer think it's the best way to describe it, though.

I hope this helps!
Richard