[ghc-steering-committee] Proposal: Embrace Type in Type

[Iavor Diatchki]

>From the GitHub discussions and the e-mails, I've seen a couple of other
options being proposed/discussed:

   * Use a unicode star operator.
      - Pros: short, looks like the current star, much less likely to clash
with stuff.
      - Cons:  typing a unicode symbol in some editors could be a pain.

   * Continue using `*` (or another infix operator), but require that it be
written in prefix notation, i.e. write `(*)` instead of `*`.
      - Pros: less of a wart, follows normal language rules
      - Cons: it is odd to use an infix operator that is not binary (i.e.,
can't be written infix);  still uses up the `*` name

    * Continue using `*` but---at the type level---have it always refer to
the kind, when used unqualified. This is what is called `StartIsKind` in
the proposal.


On Wed, Feb 21, 2018 at 7:59 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> The issue about ‘*’ seems to be this
>
>
>
>    - We need a way to write down the kind of types.   E.g.    Int :: ???
>
> What is the “???”
>
>
>
> ·        There are several possibilities
>
> 1.      Continue to use * as *built in syntax.  *It’s a massive wart; you
> can’t write (*->*) because GHC thinks that’s a single lexeme;  and * is a
> terrifically useful infix operator, so stealing it is horrible.   I’m sure
> we would never do this today.
>
> 2.      Import a module Data.Type to bring  Type into scope using the *normal
> module scoping mechanism*.
>
>    - Advantage: no new special things
>          - Disadvantage: an extra import; and error messages might say
>          Data.Type.Type fully qualified if you didn’t have the import.
>
> 3.      Same, but export Type from Prelude.
>
>    - Advantage: no need for that special import
>          - Disadvantage: would break existing programs that define Type,
>          and import Prelude, regardless of flags.
>
> I suppose we could say that you only get Type from Prelude if -XTypeInType
> is also on, but that IS new (and ad hoc) mechanism.
>
> 4.      Define Type as a new *keyword* (with TypeInType).  It does not
> need to be imported; it cannot be overridden or redefined.  (Just like
> (->).)
>
>    - A variant of this (which I quite like) is to use the existing
>          keyword *type* (lowercase).
>          - Advantage: simple clear story
>          - Note: won’t break existing code; only code that says TypeInType
>
> Is that a fair summary of the design space?
>
> Simon
>
>
>
>
>
> *From:* Iavor Diatchki [mailto:iavor.diatchki at gmail.com]
>
> *Sent:* 09 February 2018 17:47
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
>
> *Cc:* Richard Eisenberg <rae at cs.brynmawr.edu>;
> ghc-steering-committee at haskell.org; Joachim Breitner <
> mail at joachim-breitner.de>
>
>
> *Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type
>
>
>
> The issue I see is that it is quite common to get a kind error without
> doing any fancy type level programming---in particular without writing kind
> signatures or anything like that.  So you'd have no reason to import
> `Data.Kind(Type)`.    The result would be that GHC would give quite a
> verbose error message, using the fully qualified name of `Type`.  Unless we
> did something special.
>
>
>
> -Iavor
>
>
>
>
>
> On Fri, Feb 9, 2018 at 2:41 AM Simon Peyton Jones <simonpj at microsoft.com>
> wrote:
>
> I’m not sure I see the problem here.  If ‘Int’ is not in scope then
>
> f :: Int -> Int
>
> won’t work.  What’s different about ‘Type’
>
>
>
> Simon
>
>
>
> *From:* ghc-steering-committee [mailto:
> ghc-steering-committee-bounces at haskell.org] *On Behalf Of *Richard
> Eisenberg
> *Sent:* 09 February 2018 04:26
> *To:* Iavor Diatchki <iavor.diatchki at gmail.com>
> *Cc:* ghc-steering-committee at haskell.org; Joachim Breitner <
> mail at joachim-breitner.de>
> *Subject:* Re: [ghc-steering-committee] Proposal: Embrace Type in Type
>
>
>
> Thanks, Iavor, for bringing this up.
>
>
>
> To clarify the proposal: -XStarIsType is orthogonal to deprecation. The
> extension is necessary in order to continue to parse existing programs, but
> if we choose to deprecate *, then we would deprecate even with -XStarIsType
> is enabled (precisely to avoid the half-deprecation scenario Iavor is
> worried about).
>
>
>
> I envisioned always printing Type unqualified in error messages, even if
> it's not imported. If a user writes Type and it's out of scope, we could
> always have a special-case check suggesting they import Data.Kind. I won't
> argue this is a principled design, though, and is likely a poor choice if
> some other Type is in scope.
>
>
>
> The truth is that I don't have a great way forward here (and haven't for
> years) and am very hopeful someone on this list can come up with one! :)
> The proposal has my best idea, but I'm still not thrilled with it.
>
>
>
> Thanks,
>
> Richard
>
>
>
> On Feb 8, 2018, at 1:46 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
>
>
> Hello,
>
>
>
> I didn't see any discussion about the third part of this proposal, namely
> the addition of a new extension called `StarIsKind`.  The idea is that when
> this is on, `*` will still be treated as a special alpha-numeric name, and
> it will *always* refer to the kind of inhabited types (i.e., same as
> know).  The difference is that it cannot be used as another type-level
> operator (e.g., for multiplication).
>
>
>
> Presumably, when this extension is on, there would be no deprecation
> warning emitted for `*`? We should clarify this in the proposal.
>
>
>
> I am not certain if this is a good idea.  It makes the use of `*` sort of
> "half" deprecated, and leaves us with multiple "standard" ways to refer to
> the same thing (e.g., in type errors).  Also, if we want people to update
> their code to use `Type` instead of `*`, then we are just delaying the pain
> point to whenever `StarIsKind` ends up being not on by default.
>
>
>
> OTOH, if we don't have a standard short-hand way to refer to the kind of
> inhabited types, I imagine GHC will report some very ugly errors.  For
> example:
>
>
>
>     • Expecting one more argument to ‘Maybe’
>
>       Expected a type, but ‘Maybe’ has kind ‘Data.Kind.Type ->
> Data.Kind.Type’
>
>
>
> And this is for a fairly simple kind error, they get much longer if, say,
> monad transformers are involved.
>
>
>
> What do others think?
>
>
>
> -Iavor
>
>
>
>
>
>
>
>
>
>
>
>
>
> On Sat, Feb 3, 2018 at 8:24 PM Richard Eisenberg <rae at cs.brynmawr.edu>
> wrote:
>
>
> > On Feb 1, 2018, at 8:58 PM, Joachim Breitner <mail at joachim-breitner.de>
> wrote:
> >
> > In particular in light of our use of “type” as a explicit namespace
> > token – so far in export and import lists and fixity declarations – I
> > worry that we will prevent ourselves from using more such explicit
> > namespace things in the future.
>
> This is a really good point. In private musings, I've often wondered about
> using the keyword `type` in expressions to denote a namespace change. More
> concretely, I'm worried about the Dreaded Namespace Problem (DNP): that is,
> a dependently typed language does not want to have separate type-level and
> term-level namespaces. Of course, Haskell has this.
>
> The best solution I have so far to the DNP is to introduce a *new*
> namespace, distinct from the two namespaces we have so far. Let's call it
> the "default" namespace. When -XDependentTypes is on, the default namespace
> is in effect. Name lookup looks first in the default namespace. If that
> fails the namespace consulted next depends on context: the "data" namespace
> in terms and the "type" namespace in type signatures. (This last bit needs
> to be specified more concretely, but you get the idea.) Or, perhaps, a
> failed lookup in the default namespace will look up in both the type and
> data namespaces, erroring if a name appears in both.
>
> If a user wants to specify a namespace directly, they have a very easy way
> to do so: `type Foo` will look in the type namespace, `data Foo` will look
> in the data namespace, and `default Foo` will look in the default
> namespace. :) Because these keywords make sense currently only at the
> beginning of a line, this Just Works. I also imagined these constructs
> could scope over a subexpression: `type (T S)`.
>
> All of this deserves a proper proposal and it's too early for that
> proposal. Nevertheless, I'm grateful that Joachim said something here,
> given that adding `type` as a spelling of `Type` would invalidate this
> approach. I also am swayed by the fact that `Type` isn't fully primitive,
> and making a keyword mean something that's not primitive is a bit awkward.
> I thus retract this proposed alternative and will update the proposal
> accordingly.
>
> 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/20180221/fa405338/attachment-0001.html>