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

[Iavor Diatchki]

Hello,

These are significant changes to the current terminology and I really don't
think that this is the right place to discuss them---I think that they are
significant enough that they deserve their own proposal, with motivation,
and discussion by the community.

Here are some things to think about, if such a proposal is ever written:
  * in this new terminology `4` is not a type, but it also does not fall in
any of the other categories, so what is it?
  * how about `Eq`?
  * how about a type variable `f`?
  * are type functions really type constructors?
  * are we really suggesting that we should start supporting things like
`'True` at the value level?

Anyway, it seems to me that we have gone a little off-course, and these
changes are not really about making #106 easier to understand.

-Iavor


On Fri, Aug 17, 2018 at 6:46 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

>
>
> On Aug 17, 2018, at 3:22 AM, Simon Peyton Jones via ghc-steering-committee
> <ghc-steering-committee at haskell.org> 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
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180820/f06d10b5/attachment.html>