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

[Richard Eisenberg]

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 <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/ <http://www.joachim-breitner.de/>
> _______________________________________________
> 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
> 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/20180524/25c6f819/attachment.html>