Open data kinds

[Richard Eisenberg]

Janek and I discussed this issue this morning, and I would like to state my opinion and state my case:

 * In `kind K = T`, `T` should live in the data-level namespace.

Of course, if `T` is used in a term-level expression, an error should be issued, because T logically lives only in types.

To explain why I feel this way, it's helpful to reflect on the 4 namespaces Haskell currently has. I will refer to these by number.

1. Term-level data constructors and pattern synonyms
2. Types, classes, and type constructors
3. Term-level variables and globals
4. Type variables

The debate at hand only involves 1 and 2. We are adding a new feature to the language. Should it go in namespace 1 or namespace 2? To help decide, it would be nice to have a general principle of what goes in 1 and what goes in 2. Here is one possible principle:

A. Namespace 1 contains runtime things; namespace 2 contains compile-time things.

Principle A has served us well for some time. But it's failing us now. With DataKinds, we can use namespace-1 things at compile-time. And some of us have been scheming for a way to use namespace-2 things at runtime. So Principle A doesn't seem quite right. Instead, I propose

B. Namespace 1 contains data constructors (and, closely related, pattern synonyms); namespace 2 contains datatypes (and, closely related, classes).

Up until DataKinds, Principles A and B have coincided. But now they have diverged, and only Principle B serves to describe what's going on.

(Aside: When you say True in a type, and it's in scope, that's because GHC looks in namespace 2 first; failing that, it looks in namespace 1. DataKinds never copies namespace-1 things into namespace 2.)

If we thus adopt Principle B, then we indeed want `T` from the example to live in namespace 1. It is a data constructor. One might argue that this is a misnomer, because T lives only at compile time. T indeed does live only at compile time, but it still is a data constructor -- it constructs compile-time data. (Just like using 'True in a type doesn't make 'True any less of a data constructor.)

A noted drawback of Principle B is that it means that compile-time only definitions "pollute" namespace 1. That's true. But it need be only local, as you're free to make namespace-2 type synonyms that refer to namespace-1 data constructors. And it's quite straightforward to ensure that `T` is never present at runtime -- it's just a straightforward check in the typechecker.

Thus, according to general Principle B, `T` should be in namespace 1.

What do you think?

Richard

On Dec 16, 2015, at 2:21 PM, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:

> Devs,
> 
> I plan to work on implementing open data kinds (#11080). The idea is that users will be allowed to 
> declare open kinds and then populate them with member types. Perhaps I will also implement closed 
> data kinds. This is already possible using DataKinds, but the idea is to declare a data kind 
> without corresponding data type - see #6024.
> 
> Now, consider this declaration (syntax subject to bikeshedding):
> 
>  kind K = T
> 
> In what namespace should T go: type namespace or data constructor namespace? If we put it in type 
> namespace then it is possible for the user to declare a data constructor T that is completely 
> unrelated to type T belonging to kind K. This might be confusing. If we put T in the data 
> namespace then we miss the point of #6024.
> 
> Thoughts?
> 
> Janek
> 
> ---
> Politechnika Łódzka
> Lodz University of Technology
> 
> Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata.
> Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę
> prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie.
> 
> This email contains information intended solely for the use of the individual to whom it is addressed.
> If you are not the intended recipient or if you have received this message in error,
> please notify the sender and delete it from your system.
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>