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

[Ryan Newton]

@Manuel, for you would it be sufficient for *-deprecation to have an
*eventual* plan to put Type prelude?

I just can't see how, if Haskell were designed today, the "*" convention
would come to be.  Personally, I worry more about legacy/textbook issues
for topics that are a bit closer to CS101 than I believe kind signatures
are.

 -Ryan

On Sat, Feb 10, 2018 at 12:42 AM, Manuel M T Chakravarty <
chak at justtesting.org> wrote:

> Yes, that’s why I think, we cannot deprecate it until we have an
> alternative that is not the fully qualified name.
>
> Manuel
>
>
> Am 10.02.2018 um 04:46 schrieb Iavor Diatchki <iavor.diatchki at gmail.com>:
>
> 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
>>
>>
>>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
>
>
>
> _______________________________________________
> 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/20180210/c7cb745f/attachment-0001.html>