[ghc-steering-committee] Proposal: Define Kinds Without Promotion (#106)

[Simon Peyton Jones]

|  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 at haskell.org> On
|  Behalf Of Eric Seidel
|  Sent: 17 August 2018 00:47
|  To: ghc-steering-committee at 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 at 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 at 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 at haskell.org
|  > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-com
|  > > > mittee
|  > >
|  > > _______________________________________________
|  > > ghc-steering-committee mailing list
|  > > ghc-steering-committee at haskell.org
|  > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-commi
|  > > ttee
|  > >
|  > _______________________________________________
|  > ghc-steering-committee mailing list
|  > ghc-steering-committee at haskell.org
|  > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committ
|  > ee
|  _______________________________________________
|  ghc-steering-committee mailing list
|  ghc-steering-committee at haskell.org
|  https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee