I rewrote the wiki page to include open data kinds proposal: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindsWithoutData It would be a Good Thing to agree on the syntax before it gets implemented. So if anyone wants to express their preference or have a constuctive argument for/against some particular proposal now is a good time. I would like to start working on the implementation sometime soonish. Janek Dnia czwartek, 17 grudnia 2015, Richard Eisenberg napisał:

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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

--- 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.

There is no language support to define a "closed datatype" but it is possible to do so by not exporting any of the constructors used to make the datatype. Data types are closed in a sense that if you define

data Foo = MkFoo1 then you cannot add new data constructor, say MkFoo2, that will also create values of type Foo. So being open/closed is not about creating new values of a data type but about extending the definition with new constructors. Does that answer your question? 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.