<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Iavor brings up some really good points here. He's right that I'm (mostly) arguing about terminology. At their core, I might summarize Iavor's points as follows:<div class=""><br class=""></div><div class="">* Should we change this terminology at all?</div><div class="">* If so, should we do so now?</div><div class=""><br class=""></div><div class="">Unsurprisingly, I wish to argue "yes" to both points.</div><div class=""><br class=""></div><div class="">First off, I recognize that I'm arguing against the Haskell grain right now, in that the terminology is well established. I had not considered the use of, say, "type constructor" in the manual. (In all this, I'm thinking solely of user-facing features, not at all the GHC implementation.) I did not acknowledge this in my first email in this thread.</div><div class=""><br class=""></div><div class="">Why change the terminology?</div><div class=""><br class=""></div><div class="">- The current terminology puts us out of step with the dependent types community. The features we're discussing (i.e., the ability to use `'True' as a type argument) exist only in Haskell and in dependently typed languages. It thus seems sensible to be in line with dependently typed languages in our terminology.</div><div class=""><br class=""></div><div class="">- Calling `'True` a type leads to confusion, because some people want to find some term whose type is `'True`, but such a thing cannot exist.</div><div class=""><br class=""></div><div class="">- Currently, we say that * is the "kind of types with values". But someone could reasonably ask whether Void has kind * -- after all, Void is inhabited by no values. (It is inhabited by `undefined`, but that's not a value.) So "kind of types with values" is a bit wrong. Perhaps better would be "kind of types inhabited by terms", but that's an even wordier mouthful. With the proposed change in terminology, we could just say that * is the kind of types. Simple! (Naturally, this works beautifully with *'s new name, Type.)</div><div class=""><br class=""></div><div class="">- It's conceptually simpler (to me), to think of `'True` and `True` as the same thing. In the new terminology, both are data constructors. Indeed, we can refer to them as being the same -- the ' is there because the two appear in different contexts and therefore must be spelled slightly differently (like we understand M.lookup and Map.lookup to be the same thing but with different import statements in scope). By describing the two as the same, we have better intuition around, e.g., export/import lists, where there would no longer be a desire to export/import the "type constructor" independently of the "data constructor".</div><div class=""><br class=""></div><div class="">- Right now, datatypes and data families have a restriction that their kinds end in `... -> *`. With the new terminology, we can just say these must be type constructors.</div><div class=""><br class=""></div><div class="">- GHC uses this terminology in a limited way in error messages. If you say `x :: 'True`, GHC says that True is expected to be a type. According to the "old" terminology, `'True` *is* a type, so this error message is misleading. Under the new terminology, it works just fine.</div><div class=""><br class=""></div><div class="">Reasons to keep the existing terminology:</div><div class=""><br class=""></div><div class="">- It's existing. This means that it's familiar to many and has been enshrined in written materials.</div><div class=""><br class=""></div><div class="">- Many find the type-leve/term-level distinction to be a convenient proxy for the compile-time/runtime distinction. In today's Haskell, this is accurate, though it would change with dependent types. However, my suggested change in terminology does not change this -- it just means that data constructors can be used at the type level.</div><div class=""><br class=""></div><div class="">We should also consider the timing of this change. Why do this now instead of waiting?</div><div class=""><br class=""></div><div class="">- The new terminology makes as good sense today as it will in a dependently typed future. Even if the development toward dependent types stops, this change is worthwhile for the reasons above, none of which appeal to any features that do not already exist.</div><div class=""><br class=""></div><div class="">- The right time for any change of this sort is "yesterday". But seeing as we can't do that, let's do "today", the next best thing.</div><div class=""><br class=""></div><div class="">Essentially, my argument here is that we got this all slightly wrong when -XDataKinds came into being -- not the feature, but the way we describe it. Perhaps this is all just much ado about little, but I do think this small change in how we speak of these features will help Haskellers learn how they work with the right set of intuitions.</div><div class=""><br class=""></div><div class="">(I would like to note that my arguments here are borne of experience. I was not part of the initial wave of design of -XDataKinds, but if I had been, I'm sure I would have gone with what I'm calling the "old" terminology.)</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div><div class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 16, 2018, at 6:02 AM, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class="">Hello,<div class=""><br class=""></div><div class="">I'd be happy to make changes to the text of the proposal, but I would like to understand the underlying concerns so that I can address them appropriately. At the moment, I am pretty sure that I am missing something, as might be evident from my comments below. Either way, my comments below are intended to shed some light on my thinking, and emphasize the parts of Richard's comments I don't understand.</div><div class=""><br class=""></div><div class=""><div class="gmail_quote"></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div dir="ltr" class="">On Wed, Aug 15, 2018 at 6:10 AM Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" target="_blank" class="">rae@cs.brynmawr.edu</a>> wrote:<br class=""></div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;"><br class="">- Types and kinds are simply the same now. There really is no difference. So the first sentence of this proposal, "This proposal introduces a language construct for defining kinds without having to promote types." is, in my opinion, quite misleading.</blockquote><div class=""> </div><div class="">The proposal uses the same terminology that is used in GHC's manual, and also by the majority of the Haskell community. For example, Section 10.1 of the manual is about "Datatype Promotion", and the summary is "Allow promotion of data types to kind level.". Section 10.10.2 says "With DataKinds, GHC automatically promotes every datatype to be a kind and its (value) constructors to be type constructors.". This proposal introduces a language construct that allows us to declare non-empty kinds without having to promote a datatype in the sense of 10.1. I am talking about the language specification, not the actual implementation, which we can discuss once we agree we'd like to have this new feature.</div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""><br class=""></div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">All `data` declarations introduce kinds (because they introduce types, and types = kinds). And data constructors aren't really promoted either -- they can simply be used in types.<br class=""></blockquote><div class=""><br class=""></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class="">Of course this is technically correct, but without data type promotion these are empty kinds that are a side-effect of mixing up types and kinds. I say empty "kinds" rather than empty "types" to emphasize the fact that I am referring to the kinding relation, not the typing one.</div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""><br class=""></div><div class=""> </div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">- The proposal talks about referring to types in export lists. But we can already do this, via the normal syntax for listing data constructors with type constructors. So I'm not sure what that point of motivation really means.<br class=""></blockquote><div class=""><br class=""></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class="">Here is a datatype declaration:</div><div class=""><br class=""></div><div class="">data T = A | B</div><div class=""><br class=""></div><div class="">In current GHC how would you export the type `A` of kind `T` without exporting the value `A` of type `T`?</div><div class=""><br class=""></div><div class="">Here is my attempt:</div><div class=""><br class=""></div><div class=""><div class="">{-# Language DataKinds, ExplicitNamespaces #-}</div><div class=""> </div><div class="">module M (type A) where</div><div class=""><br class=""></div><div class="">data T = A | B</div></div><div class=""><br class=""></div><div class="">This results in:</div><div class=""><div class=""><br class=""></div><div class="">error: Not in scope: type constructor or class ‘A’</div><div class=""> |</div><div class="">3 | module M (type A) where</div><div class=""> <span class="Apple-converted-space"> </span>| ^^^^^^</div></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""><br class=""></div><div class=""><br class=""></div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">- The "normal types win" is true, but it's all about namespace lookup. In a type, when GHC sees a capitalized identifier, it looks in the type namespace for that identifier. If the identifier is bound in the type namespace, that identifier is found. If not, GHC looks in the data-level namespace. According to this algorithm, "normal types win", indeed. But the "normal"cy of the type is that it lives in the type namespace, not because it isn't promoted.<br class=""></blockquote><div class=""><br class=""></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class="">I think that with this proposal we have a much easier way to explain how things work, without having to refer to the algorithm used by GHC's renamer:</div><div class=""><br class=""></div><div class="">data T = A | B -- T is a type, and A and B are values of this type</div><div class="">type data S = X | Y -- S is a kind, and X and Y are types of this kind</div><div class=""><br class=""></div><div class="">Simple.</div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""> </div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">- If something introduced with `type data` can be used without -XDataKinds, then what does -XDataKinds really mean? It would seem to enable solely the extra data-level namespace check. That's fine with me, but we should document it that way. Alternatively, -XDataKinds could mean that some types have kinds that don't end in Type or Constraint, in which case it would need to be enabled to use a `type data` data constructor.<br class=""></blockquote><div class=""><br class=""></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class="">This proposal is orthogonal to `DataKinds` and does not change anything about how it works. </div><div class=""><br class=""></div><div class="">Personally, if I had `TypeData`, I think I would very rarely use `DataKinds`, except for type-level nats and symbols, which should probably get a separate extension anyway. The reason is that I rarely need the same constructors at the value and the type level without any link between the two.</div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""> </div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">- The RHS of a `type data` does not introduce type constructors. A type constructor constructs a type -- that is, if T is a type constructor, then T applied to appropriate arguments has kind Type (or Constraint). But the data constructors of `type data` really are data constructors. It just so happens that their names live only in the type-level namespace. If we want, we can call these "type-level data constructors", but I think "type constructors" is misleading.<br class=""></blockquote><div class=""><br class=""></div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class="">I am sorry but I don't understand this at all---it is going contrary to the terminology used by the Haskell community for decades. I really don't see why we need to invent new terms, and arbitrarily limit the term "type-constructor" to only types of kind `Type` or `Constraint`, especially if we are willing to refer to all "kinds" as "types". The notion of classifying types by kinds and having a rich kind language is completely orthogonal to dependent types, and I think the current terminology works just fine.</div><div class=""><br class=""></div><div class="">If I am reading Richard's comments correctly (and I apologize if I am misunderstanding) his main concern is about terminology, based on his vision and plans about Dependent Haskell. I am supportive of work in this area, but I don't think that this proposal is the right place to start changing the terminology. I would suggest that we stick with the established language, which is widely used by the community, GHC's manual, and GHC's source code. Once there is a design document for Dependent Haskell, we could discuss that and settle on appropriate terminology.</div><div class=""><br class=""></div><div class="">-Iavor</div></div></div></div><div dir="ltr" class=""><div class=""><div class="gmail_quote"><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""> </div><blockquote class="gmail_quote" style="margin: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;">Thanks,<br class="">Richard<br class=""><br class="">> On Aug 14, 2018, at 8:31 PM, Eric Seidel <<a href="mailto:eric@seidel.io" target="_blank" class="">eric@seidel.io</a>> wrote:<br class="">><span class="Apple-converted-space"> </span><br class="">> Hi everyone!<br class="">><span class="Apple-converted-space"> </span><br class="">> This proposal would allow the declaration of new kinds and type constructors, without the associated data constructors that would have been generated by -XDataKinds.<br class="">><span class="Apple-converted-space"> </span><br class="">><span class="Apple-converted-space"> </span><a href="https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0000-type-data.rst" rel="noreferrer" target="_blank" class="">https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0000-type-data.rst</a><br class="">><span class="Apple-converted-space"> </span><br class="">> It introduces a new language extension, -XTypeData, which allows declarations like the following:<br class="">><span class="Apple-converted-space"> </span><br class="">> type data Universe = Character | Number | Boolean<br class="">><span class="Apple-converted-space"> </span><br class="">> This introduces a new kind, Universe, with three associated type constructors<br class="">><span class="Apple-converted-space"> </span><br class="">> Character :: Universe<br class="">> Number :: Universe<br class="">> Boolean :: Universe<br class="">><span class="Apple-converted-space"> </span><br class="">> Notably, no data constructors are introduced.<br class="">><span class="Apple-converted-space"> </span><br class="">> The proposal aims to solve several usability issues with -XDataKinds:<br class="">><span class="Apple-converted-space"> </span><br class="">> 1. We often don't want the data constructors, which simply pollute the value namespace.<br class="">> 2. We cannot easily control the export behavior of promoted types (instead we resort to tricks like the alias `type Character = 'Character`).<br class="">> 3. The name resolution rules involving promoted types can be confusing.<br class="">><span class="Apple-converted-space"> </span><br class="">> I find these issues (particularly #2) compelling, and the community response seems to be mostly positive, so I recommend accepting the proposal.<span class="Apple-converted-space"> </span><br class="">><span class="Apple-converted-space"> </span><br class="">> I'm not particularly fond of the proposed syntax (`type data` makes it sound like we're doing something with data constructors, which is precisely what we're NOT doing), but the proposal has already had a good bit of bikeshedding, and people seem mostly happy with the current syntax, so I think we should probably stick with `type data`.<br class="">><span class="Apple-converted-space"> </span><br class="">> Eric<br class="">> _______________________________________________<br class="">> ghc-steering-committee mailing list<br class="">><span class="Apple-converted-space"> </span><a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a><br class="">><span class="Apple-converted-space"> </span><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br class=""><br class="">_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" target="_blank" class="">ghc-steering-committee@haskell.org</a><br class=""><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br class=""></blockquote></div></div></div></div><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">_______________________________________________</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">ghc-steering-committee mailing list</span><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><a href="mailto:ghc-steering-committee@haskell.org" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">ghc-steering-committee@haskell.org</a><br style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a></div></blockquote></div><br class=""></div></div></body></html>