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

Wed Jun 20 21:14:52 UTC 2018

I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148 <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 <mailto: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 <mailto: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 <mailto:iavor.diatchki at gmail.com>>
> Cc: ghc-steering-committee at haskell.org <mailto:ghc-steering-committee at haskell.org>; Joachim Breitner <mail at joachim-breitner.de <mailto: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 <mailto: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 <mailto: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 <mailto: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 <mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee>
> _______________________________________________
> ghc-steering-committee mailing list
> ghc-steering-committee at haskell.org <mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee <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/20180620/15a9b7fc/attachment.html>