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

[Eric Seidel]

I'm happy to request clarification, but first I'd like to clarify a few things for myself :)

On Tue, Aug 14, 2018, at 23:09, Richard Eisenberg wrote:
> - The proposal talks about referring to types in export lists. But we 
> can already do this, via the normal syntax for listing data constructors 
> with type constructors. So I'm not sure what that point of motivation 
> really means.

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.

> - The "normal types win" is true, but it's all about namespace lookup. 
> In a type, when GHC sees a capitalized identifier, it looks in the type 
> namespace for that identifier. If the identifier is bound in the type 
> namespace, that identifier is found. If not, GHC looks in the data-level 
> namespace. According to this algorithm, "normal types win", indeed. But 
> the "normal"cy of the type is that it lives in the type namespace, not 
> because it isn't promoted.
> 
> - If something introduced with `type data` can be used without -XDataKinds,
> then what does -XDataKinds really mean? It would seem to 
> enable solely the extra data-level namespace check. That's fine with me, 
> but we should document it that way. Alternatively, -XDataKinds could 
> mean that some types have kinds that don't end in Type or Constraint, in 
> which case it would need to be enabled to use a `type data` data 
> constructor.

I think I agree with both of these points.

> - Types and kinds are simply the same now. There really is no 
> difference. So the first sentence of this proposal, "This proposal 
> introduces a language construct for defining kinds without having to 
> promote types." is, in my opinion, quite misleading. All `data` 
> declarations introduce kinds (because they introduce types, and types = 
> kinds). And data constructors aren't really promoted either -- they can 
> simply be used in types.

True, it's misleading to say that types are promoted to kinds (though, as you've mentioned elsewhere, the distinction is still quite useful for us humans), but I don't think it's misleading to say that data constructors are promoted to type constructors. See below.

> - The RHS of a `type data` does not introduce type constructors. A type 
> constructor constructs a type -- that is, if T is a type constructor, 
> then T applied to appropriate arguments has kind Type (or Constraint). 
> But the data constructors of `type data` really are data constructors. 
> It just so happens that their names live only in the type-level 
> namespace. If we want, we can call these "type-level data constructors", 
> but I think "type constructors" is misleading.

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. We still have a value/type level distinction in Haskell, so the term "type-level data constructor" reads like an oxymoron to me. 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 realize that these "type-level data" constructors are probably still represented in GHC with `DataCon`s, but I think my classification is probably more useful from an end-user perspective.)

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. 

I look forward to being corrected!