| I know we generally operate on the silence-means-agreement principle, but | this disagreement is over a pretty crucial definition, so I'd like to | solicit feedback from the rest of the committee. Can you restate the terminological choice(s) as explicitly as possible, with examples? Simon | -----Original Message----- | From: ghc-steering-committee <ghc-steering-committee-bounces@haskell.org> On | Behalf Of Eric Seidel | Sent: 17 August 2018 00:47 | To: ghc-steering-committee@haskell.org | Subject: Re: [ghc-steering-committee] Proposal: Define Kinds Without | Promotion (#106) | | It sounds like we all agree that the disagreement is mostly over | terminology, specifically, over the definition of a type constructor. | Richard prefers a definition that limits type constructors to producing | objects of type Type (or Constraint), whereas I (and Iavor, I think) prefer | a broader definition that encompasses any constructor that produces an | object that can be used at the type-level. Richard points out, correctly, | that when Dependent Haskell arrives, the value/type level distinction will | disappear, and our definition will become (mostly) untenable. (I say mostly | because, at least in my limited experience with dependent types, you often | still have objects that are used primarily in a type context, and so an | informal value/type distinction could still be useful.) | | The question then is what to do in the meantime. Do we stick with the | established terminology and incur a larger change when Dependent Haskell | arrives, or do we start making preparations now? I think Richard's | perspective makes sense for a dependently-typed language, but Haskell is not | dependently-typed, yet. So I'm inclined to say the change of terminology | should be deferred to the Dependent Haskell proposal. | | I know we generally operate on the silence-means-agreement principle, but | this disagreement is over a pretty crucial definition, so I'd like to | solicit feedback from the rest of the committee. | | On Thu, Aug 16, 2018, at 06:02, Iavor Diatchki wrote: | > Hello, | > | > 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. | > | > On Wed, Aug 15, 2018 at 6:10 AM Richard Eisenberg | > <rae@cs.brynmawr.edu> | > wrote: | > | > > | > > - 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. | > | > | > 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. | > | > 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. | > > | > | > 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. | > | > | > | > > - 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. | > > | > | > Here is a datatype declaration: | > | > data T = A | B | > | > In current GHC how would you export the type `A` of kind `T` without | > exporting the value `A` of type `T`? | > | > Here is my attempt: | > | > {-# Language DataKinds, ExplicitNamespaces #-} | > | > module M (type A) where | > | > data T = A | B | > | > This results in: | > | > error: Not in scope: type constructor or class ‘A’ | > | | > 3 | module M (type A) where | > | ^^^^^^ | > | > | > - 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. | > > | > | > 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: | > | > data T = A | B -- T is a type, and A and B are values of this type | > type data S = X | Y -- S is a kind, and X and Y are types of this kind | > | > Simple. | > | > | > > - 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. | > > | > | > This proposal is orthogonal to `DataKinds` and does not change | > anything about how it works. | > | > 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. | > | > | > > - 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. | > > | > | > 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. | > | > 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. | > | > -Iavor | > | > | > | > | > | > | > | > > Thanks, | > > Richard | > > | > > > On Aug 14, 2018, at 8:31 PM, Eric Seidel <eric@seidel.io> wrote: | > > > | > > > Hi everyone! | > > > | > > > This proposal would allow the declaration of new kinds and type | > > constructors, without the associated data constructors that would | > > have been generated by -XDataKinds. | > > > | > > > | > > https://github.com/yav/ghc-proposals/blob/data-kind-only/proposals/0 | > > 000-type-data.rst | > > > | > > > It introduces a new language extension, -XTypeData, which allows | > > declarations like the following: | > > > | > > > type data Universe = Character | Number | Boolean | > > > | > > > This introduces a new kind, Universe, with three associated type | > > constructors | > > > | > > > Character :: Universe | > > > Number :: Universe | > > > Boolean :: Universe | > > > | > > > Notably, no data constructors are introduced. | > > > | > > > The proposal aims to solve several usability issues with -XDataKinds: | > > > | > > > 1. We often don't want the data constructors, which simply pollute | > > > the | > > value namespace. | > > > 2. We cannot easily control the export behavior of promoted types | > > (instead we resort to tricks like the alias `type Character = | 'Character`). | > > > 3. The name resolution rules involving promoted types can be | confusing. | > > > | > > > I find these issues (particularly #2) compelling, and the | > > > community | > > response seems to be mostly positive, so I recommend accepting the | > > proposal. | > > > | > > > 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`. | > > > | > > > Eric | > > > _______________________________________________ | > > > ghc-steering-committee mailing list | > > > ghc-steering-committee@haskell.org | > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-com | > > > mittee | > > | > > _______________________________________________ | > > ghc-steering-committee mailing list | > > ghc-steering-committee@haskell.org | > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-commi | > > ttee | > > | > _______________________________________________ | > ghc-steering-committee mailing list | > ghc-steering-committee@haskell.org | > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ | > ee | _______________________________________________ | ghc-steering-committee mailing list | ghc-steering-committee@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee