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

On Aug 17, 2018, at 3:22 AM, Simon Peyton Jones via ghc-steering-committee wrote:

Can you restate the terminological choice(s) as explicitly as possible, with examples?

Old: type: Something used at the type level. In contrast to "type constructor", generally doesn't take any arguments. Examples: Int, Bool, 4, 'True, '[Int, Bool], '[] type constructor: Something used in a function position in a type. Examples: Maybe, Either, 'Just data constructor: A symbol used to construct a data element of some type at runtime. Examples: True, Nothing, Left. Non-examples: 'True, 'Nothing, 'Left. promotion: 'True is a type that is the promoted form of the data constructor True; 'Just is a type constructor that is the promoted form of the data constructor Just. New: type: Something that can reasonably go to the right of a ::. In other words, an element of the kind * (or Type). Examples: Int, Bool, Maybe Double. Non-examples: 4, 'True, '[Int, Bool], '[] type constructor: Something that, when applied to the right number of well-kinded arguments, becomes a type. Examples: Maybe, Either. Non-example: 'Just data constructor: A symbol used to construct a data element of some type, at either runtime or compile-time. Examples: True, Nothing, Left, 'True, 'Nothing, 'Left. promotion: No longer used. 'True and True are now the same thing: both data constructors, just used in different contexts. NB: This is all about user-facing documentation. I am not proposing any change to GHC datatypes. I hope this helps! Richard