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

Fri Jun 29 18:25:52 UTC 2018

I am supportive of accepting the proposal, but I think that we should
address the point raised by Joachim on the the git-hub thread first  (
https://github.com/ghc-proposals/ghc-proposals/pull/99#issuecomment-401060976).
It really is not quite clear if the specificity is a property of the type
itself, or the thing that has that type.

On Thu, Jun 28, 2018 at 1:07 AM Simon Peyton Jones <simonpj at microsoft.com>
wrote:

> I’m keen on this proposal. I am very keen to be able to express in a type
> or kind signature everything needful to use the value (or type
> constructor).   The proposal gives an example at the term level.  It’d be
> strengthened by an example at the type level.  Eg
>
> type T1 :: forall {k}. (k->Type) -> k -> Type
>
> data T1 f a = MkT (f a)
>
>
>
> type T2 :: forall k. (k->Type) -> k -> Type
>
> data T2 f (a::k) = MkT2 (f a)
>
>
>
> Here T1 has an inferred kind variable, mentioned nowhere in the
> declaration.  The kind signature (which I have written as if it were code,
> which is the subject of a separate proposal) is inferred as shown.
>
>
>
> T2 mentions k, so its kind signature looks a bit different.
>
>
>
> What’s the difference?  It’s exactly in explicit kind application. You can
> write  (T1 @Type Maybe Int), but T2 can’t have that explicit kind argument.
>
>
>
> The whole business of Required/Specified/Inferred is more complicated than
> I like, but if we have it (which we do right now) we should allow the
> programmer to specify exactly what they mean.
>
>
>
> (An alternative is to abolish the Specified/Inferred distinction, but that
> carries significant costs of its own and no one is proposing it.)
>
>
>
> Let’s accept!
>
>
>
> Simon
>
>
>
> *From:* Richard Eisenberg <rae at cs.brynmawr.edu>
> *Sent:* 28 June 2018 05:45
> *To:* Iavor Diatchki <iavor.diatchki at gmail.com>
> *Cc:* Simon Peyton Jones <simonpj at microsoft.com>;
> ghc-steering-committee at haskell.org; Joachim Breitner <
> mail at joachim-breitner.de>
>
>
> *Subject:* Re: [ghc-steering-committee] Discussion on proposal #99:
> forall {k}
>
>
>
> 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
> <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0015-type-level-type-applications.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=%2B7wS%2F75AielivG1KfFAzGPXKSS5aHOtEVwy9Q6WyYLU%3D&reserved=0>
> 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
> <https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F148&data=02%7C01%7Csimonpj%40microsoft.com%7C15fcb1b642114e05f1a808d5dcb1e5ca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636657578984502957&sdata=RQ4V%2FWdRz009o6sieAUpx7wQ6RCqWydsQGbENvHFZfM%3D&reserved=0>
>
>
>
> 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/20180629/7dd6881a/attachment-0001.html>