Open data kinds

[Matthew Pickering]

Jan,

Is there a specific reason for implementing closed data kinds?

The way I have been thinking about open data kinds is that they should
be like defining types. 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. To be clear, by doing so
external modules can't create more values of the type, much like
consumers can't 'extend' the kind if the library author has define a
closed data kind.

Is the same not possible here? Am I misunderstanding the proposal?

Matt

On Sun, Jan 3, 2016 at 1:31 PM, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:
> 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 <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
>
>
>
> ---
> 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