[ghc-steering-committee] Discussion on proposal #99: forall {k}

Thu Jun 28 05:27:13 UTC 2018

Ok, in that case it makes sense.   Perhaps we should update the proposal to
specify the rules that would allow me to compute the difference between
`T2` and `T3`.  Presumably there are similar rules for type families, data
families, and classes?

Once we've clarified this, I think we can accept this, unless there are any
objections.

On Wed, Jun 27, 2018 at 9:44 PM Richard Eisenberg <rae at cs.brynmawr.edu>
wrote:

> But we morally *do* have explicit kind application. See accepted proposal
> https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-type-level-type-applications.rst
> So the only reason that we don't have it is that GHC hasn't caught up to
> its specification. (I have a student working on this now.)
>
> The reason that T2 and T3 are different here is that T2 mentions the k in
> the type declaration, while T3 mentions it only in the constructor
> declaration.
>
> Richard
>
>
> On Jun 26, 2018, at 6:52 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
> wrote:
>
> Hello,
> thanks for the revisions---I read through the new version, and I think I
> almost understand the plan.   I would say that for this proposal it makes
> more sense to just deal with explicit specificities at the value level, and
> never have the curly braces in type constructors.   Since we don't have an
> explicit kind application at the type level (e.g., we can't write `Proxy
> @Type`), I don't think it really makes sense to add the braces to type
> constructors.   If we ever implemented THAT feature, then we can discuss
> which declarations should have explicit and which should have implicit
> parameters.  In the current set of examples, I find it odd that `T2` does
> not have braces, but `T3` does.
>
> -Iavor
>
>
>
>
>
>
> On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg <rae at cs.brynmawr.edu>
> wrote:
>
>> I have posted the new proposal, at
>> https://github.com/ghc-proposals/ghc-proposals/pull/148
>>
>> I've also updated #99 to clarify where the new syntax is allowed.
>>
>> For Iavor's examples:
>>
>> data T1 a = C1 a
>>
>>
>> type T1 :: Type -> Type
>> C1 :: forall a. a -> T1 a
>>
>> data T2 (a :: k) = C2 { f2 :: Proxy a }
>>
>>
>> type T2 :: forall k. k -> Type
>> C2 :: forall k (a :: k). Proxy a -> T2 a
>> f2 :: forall k (a :: k). T2 a -> Proxy a
>>
>> data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a
>>
>>
>> type T3 :: forall {k}. k -> Type
>> C3 :: forall k (a :: k). Proxy a -> T3 a
>>
>> data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a
>>
>>
>> type T4 :: forall {k}. k -> Type
>> C4 :: forall {k} (a :: k). Proxy a -> T3 a
>>
>> data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a
>>
>>
>> Rejected, as k is used dependently but is not lexically dependent. (This
>> is no change.) It we have
>>
>> > data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a
>>
>> we would get
>>
>> type T5 :: forall k -> k -> Type
>> C5 :: forall k (a :: k). Proxy a -> T5 k a
>>
>> data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a
>>
>>
>> Rejected, like T6. If we revise to:
>>
>> > data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a
>>
>> we get
>>
>> type T6 :: forall k -> k -> Type
>> C6 :: forall {k} (a::k). Proxy a -> T6 k a
>>
>> I've updated the proposal itself to include these examples.
>>
>> Does this help to clarify?
>>
>> Richard
>>
>> On May 25, 2018, at 1:56 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
>> wrote:
>>
>> Hello,
>>
>> well, I thought that Richard was going to write a new proposal based on
>> the feedback here, but it sounds like he is planning to revise #99, and
>> then write a separate new one.    I guess we should discuss the proposal
>> again once the changes are in.   I would encourage Richard to add some text
>> and examples to clarify exactly what's in the proposal and what's not, and
>> how things are supposed to work.  Here are some examples, for which it
>> would be illuminating (to me) to see the types/kinds of all names
>> introduced.
>>
>> data T1 a = C1 a
>> data T2 (a :: k) = C2 { f2 :: Proxy a }
>> data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a
>> data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a
>> data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a
>> data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a
>>
>> -Iavor
>>
>>
>> On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones <simonpj at microsoft.com>
>> wrote:
>>
>>> I’m keen to get #99 into GHC in some form.
>>>
>>>
>>>
>>> My motivation (which could be a fourth bullet in the proposal) is that
>>> it should be possible for a programmer to write a fully-explicit type
>>> signature for anything GHC can infer.  But currently we can’t.  For
>>> typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it
>>> down.
>>>
>>>
>>>
>>> based on the discussion so far, it seems that #99 in its current form
>>> might not be exactly what we want
>>>
>>>
>>>
>>> Can you summarise the reasons it might not be exactly what we want?
>>>
>>>
>>>
>>> Simon
>>>
>>>
>>>
>>> *From:* ghc-steering-committee <
>>> ghc-steering-committee-bounces at haskell.org> *On Behalf Of *Richard
>>> Eisenberg
>>> *Sent:* 24 May 2018 21:17
>>> *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] Discussion on proposal #99:
>>> forall {k}
>>>
>>>
>>>
>>> I do plan on turning Joachim's recent suggestion into a separate
>>> proposal, and then to modify #99. But the modification would remove only
>>> the bit about classes, not the feature overall. I don't have time to do
>>> this now, though -- will do next week.
>>>
>>>
>>>
>>> Richard
>>>
>>>
>>>
>>> On May 24, 2018, at 1:54 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
>>> wrote:
>>>
>>>
>>>
>>> Hello,
>>>
>>>
>>>
>>> based on the discussion so far, it seems that #99 in its current form
>>> might not be exactly what we want, so I'd say that we should reject it for
>>> the moment.   Overall, I agree that it would be nice to come up with a
>>> consistent notation for things that are currently happening in GHC but we
>>> can't write, so perhaps we could revisit this with a revised proposal at a
>>> later time?
>>>
>>>
>>>
>>> -Iavor
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>>
>>> On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <
>>> mail at joachim-breitner.de> wrote:
>>>
>>> Hi,
>>>
>>> Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg:
>>> > Joachim, you are always a fount of interesting ideas.
>>> >
>>> > > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail at joachim-breitner
>>> > > .de> wrote:
>>> > >
>>> > >   class C k (a : k) where meth :: a
>>> > >   meth :: forall {k} a. C k a -> k -> Constraint
>>> >
>>> > I think this is brilliant. But not only for this proposal! Imagine
>>> > this:
>>> >
>>> > class Num a where
>>> >   fromInteger :: Integer -> a
>>> >
>>> > fromInteger :: Integer -> forall a. Num a => a
>>> >
>>> > If we do that, then #129 is essentially solved, at no further cost to
>>> > anyone. (Note that in all Haskell98-style code, no one will ever be
>>> > able to notice the changed type of fromInteger.)
>>> >
>>> > This approach also allows for the possibility of reordering
>>> > quantified type variables for Haskell98-style constructors, if anyone
>>> > should want to do it.
>>> >
>>> > And it allows for updated types (including quantified variable
>>> > ordering, etc.) for record selectors.
>>> >
>>> > And it allows (maybe?) for giving good types to GADT record
>>> > selectors:
>>> >
>>> > data X a where
>>> >   Foo :: { bar :: Int } -> X Int
>>> >   Quux :: { bar :: Bool } -> X Bool
>>> > bar :: X a -> a
>>> >
>>> > GHC currently rejects the declaration for X, but it could be accepted
>>> > if only we could specify the correct type of bar. And now we can. I
>>> > don't particularly want to cook up the typing rules here, but I don't
>>> > think I'm totally crazy.
>>> >
>>> > GADT record selectors aside, the rule for these could be that the
>>> > top-level type signature must be equivalent w.r.t. the subtype
>>> > relation with the original type signature. That is, if the new
>>> > signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy
>>> > enough to check for. The implementation would probably do a little
>>> > worker/wrapper stunt.
>>>
>>> I smell a new proposal… what does this mean for #99? Will you want to
>>> revise it?
>>>
>>> Cheers,
>>> Joachim
>>> --
>>> Joachim Breitner
>>>   mail at joachim-breitner.de
>>>   http://www.joachim-breitner.de/
>>> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7Ca43c362fd18e4163aeba08d5c1b34be2%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636627898179266033&sdata=1cwPEVKXCcP3DuCHXOFuA%2BbEBniRLjcKI%2BAZji5vR4Q%3D&reserved=0>
>>> _______________________________________________
>>> 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/20180627/a7e61c5a/attachment-0001.html>