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