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

[Simon Peyton Jones]

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<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
_______________________________________________
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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180525/8924ae2f/attachment-0001.html>