Open data kinds

[Jan Stolarek]

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.