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

16 Aug 2018

      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 
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  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/0000-type...
...
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
...
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
value namespace.
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-committee
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee