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

[Iavor Diatchki]

My impression is that the committee overall supports the part of the
proposal where we merge `TypeInType` with `PolyKinds`.

Based on the discussion so far, opinions differ on the notation for the
kind of inhabited types (currently `*`).

-Iavor




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

> Is it true that we are supporting this proposal – except perhaps for the
> fate of “*”?    If so, let’s agree that much at least!
>
>
>
> 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/18b0a107/attachment-0001.html>