Open data kinds
eir at cis.upenn.edu
Thu Dec 17 03:55:07 UTC 2015
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?
On Dec 16, 2015, at 2:21 PM, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:
> 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.
> 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
More information about the ghc-devs