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

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 On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki Cc: ghc-steering-committee@haskell.org; Joachim Breitner 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 mailto:iavor.diatchki@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 mailto:mail@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 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@joachim-breitner.demailto:mail@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@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee