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

[Iavor Diatchki]

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/
> _______________________________________________
> 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/e2ca2881/attachment-0001.html>