[ghc-steering-committee] Please review "Visible 'forall' in types of terms" #281
Spiwack, Arnaud
arnaud.spiwack at tweag.io
Wed Nov 25 12:12:53 UTC 2020
Back to the main point, it seems to be fairly consensual, right now, that
#281 doesn't seem to have found the sweet spot which would make it work
quite right. Not yet. I basically agree with the points raised so far. As I
said earlier in the thread, I'm sympathetic with the goals, but unconvinced
by the details. Is there a committee member which disagrees with the
emerging consensus?
On Tue, Nov 24, 2020 at 1:15 PM Simon Peyton Jones via
ghc-steering-committee <ghc-steering-committee at haskell.org> wrote:
> * Having two name-spaces appears to be The Major Obstacle towards making
> satisfying incremental progress in the direction of dependent types.
>
> * So perhaps we should have an extension -XSingleNameSpace that has a
> single
> name space, with all the consequences that would entail (like changing
> the
> syntax of tuple and list types).
>
> * Then further extensions toward dependent types could require
> -XSingleNameSpace.
> If you don't want that, you don't get the new goodies. There would be no
> expectation that a dependent-types extension should fit well with the
> double-name-space situation; maybe the combination is actually
> disallowed.
>
> * Or maybe the combination is allowed, but a bit clunky. For example,
> suppose
> a library defines f :: forall a -> blah
> Then, in a module with classic-Haskell name spaces, you'd have to say
> f (type Int)
> and not (f Int), forcibly setting the namespace.
>
> It'd be good to have this conversation on GitHub, and perhaps #378 is the
> place to do that?
>
> Simon
>
> | -----Original Message-----
> | From: ghc-steering-committee <
> ghc-steering-committee-bounces at haskell.org> On
> | Behalf Of Joachim Breitner
> | Sent: 23 November 2020 08:10
> | To: ghc-steering-committee at haskell.org
> | Subject: Re: [ghc-steering-committee] Please review "Visible 'forall' in
> | types of terms" #281
> |
> | Hi,
> |
> | Richard roughly says what is my sentiment too… I’d phrase it like this:
> |
> | It seems that #281 would be rather straight forward, if it were not for
> the
> | fact that this is the first (of many?) extensions that allow types and
> terms
> | to occur in the same syntactic spot. So far, when mentally parsing a
> | program, I know where to look for types, and where to look for terms.
> #281
> | breaks that, and has to come up with lots of subtle rules, that make me
> | uneasy.
> |
> | But that's not really #281’s fault – assuming we want to head towards
> | Dependent Haskell with a unified namespace, it’s a problem that needs
> to be
> | solved! But better have that discussion with a focus on that problem,
> and
> | have a plan that works in general. Maybe #270 is the right place to have
> | that discussion.
> |
> | My impression is that all (most?) of
> | those working towards a Dependent Haskell world assume that we get a
> unified
> | namespace with no punning, and all complexity (`type` sigils, `type`-
> | qualified imports) is around compatibility with modules that use
> punning,
> | with the hope that this is rare. Few are proposing to stick to a world
> of
> | two namespaces and punning and make _that_ ergonomic. Is that impression
> | correct?
> |
> | Do local modules (#283) alleviate the punning problem a bit? Given
> `data T =
> | T`, could we make it so that T is the type and T.T the constructor?
> |
> | But this really isn't the right place to throw out shower ideas. I
> wonder if
> | it would help if someone could maintain a wiki page with an overview of
> all
> | the numerous proposals and ideas thrown around to tackle the problem
> about
> | how we get from a world of two name spaces and punning to one with one
> | namespaces and no punning.
> |
> |
> | As for #281, unless I misjudge the urgency of that change, I’d be in
> favor
> | to park it until we have a good, generally applicable plan for mixing
> terms
> | and types.
> |
> | Cheers,
> | Joachim
> |
> |
> |
> |
> | Am Montag, den 23.11.2020, 03:35 +0000 schrieb Richard Eisenberg:
> | > My silence on this proposal is because I want to accept, but I agree
> with
> | Iavor that it's become too baroque. My #378 is, in part, an attempt to
> | clarify our stance on these sorts of features so that we can take a
> stab at
> | simplifying #281 by making it less expressive.
> | >
> | > So, I guess my vote is to delay decision on this proposal until we
> have
> | one for #378 (or #270, which can also help shed light on this one).
> | >
> | > Responding directly to Alejandro's concerns here: I actually don't
> really
> | understand. I think (1) is decided by
> |
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com
> |
> %2Fghc-proposals%2Fghc-proposals%2Fblob%2Fmaster%2Fproposals%2F0081-forall-
> | arrow.rst&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e470021260
> |
> 8d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812849940%
> |
> 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi
> |
> LCJXVCI6Mn0%3D%7C3000&sdata=vU3lOmJ6kFNfEuy9MOo6ZoapadyzGIXPZblhR9QYvD0%
> | 3D&reserved=0; we use this syntax in standalone kind signatures in
> GHC
> | 8.10. We *could* change this if there were a compelling reason, but this
> | proposal is just continuing an existing feature. By (2), I think you're
> | referring to all the complications in the proposals at how to deal with
> | names and syntax in arguments -- I wouldn't myself describe this as
> | conflating the two namespaces, but rather as defining a subtle set of
> rules
> | for interpreting ambiguous names. It's the subtlety of these rules that
> | makes me uncomfortable. For (3), I don't really think there's much
> there --
> | and what there is seems to require (2) (and vice versa). Do you have an
> | example of a type-inference interaction you're worried about here?
> | >
> | > Richard
> | >
> | > > On Nov 22, 2020, at 12:09 PM, Alejandro Serrano Mena <
> trupill at gmail.com>
> | wrote:
> | > >
> | > > Hi all,
> | > > For me, there are two main concerns here:
> | > > This could be split on different proposals: (1) using the “forall a
> | > > ->” syntax, (2) conflating the type and term syntax and namespaces,
> (3)
> | introducing checking and inference for it; I find the claim that you can
> | just take the Quick Look Impredicativity paper, make a couple of
> | adjustments, and get correct checking and inference. This kind of big
> change
> | is the one for which I would actually expect a peer-reviewed paper.
> | > >
> | > > Regards,
> | > > Alejandro
> | > >
> | > > El El sáb, 21 nov 2020 a las 10:10, Joachim Breitner <mail at joachim-
> | breitner.de> escribió:
> | > > > Dear Committee,
> | > > >
> | > > > Iavor suggested to reject this proposal, but we have not heard a
> | > > > lot here yet. Especially before rejecting proposals, we probably
> | > > > owe a careful analysis, possibly with suggestions of ways forward
> | > > > (splitting the proposal into smaller pieces maybe? Iavor says
> | > > > there are many changes there).
> | > > >
> | > > > If we have continued silence, we’d reject.
> | > > >
> | > > > Cheers,
> | > > > Joachim
> | > > >
> | > > >
> | > > > Am Mittwoch, den 11.11.2020, 13:41 -0800 schrieb Iavor Diatchki:
> | > > > > Hello,
> | > > > >
> | > > > > Proposal #281 has been submitted for review by the committee
> again,
> | please read through it and let's have a discussion. Here are links to
> the
> | proposal's discussion section, and the proposal text:
> | > > > >
> | > > > >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%
> | > > > > 2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F281&da
> | > > > > ta=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e4700212608d88
> | > > > > f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741715981
> | > > > > 2849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2lu
> | > > > > MzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=oWBR%2BJue6s
> | > > > > 2bh7WU7lRhfHTcaDrQoUHzveh7e4XqWJE%3D&reserved=0
> | > > > >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%
> | > > > > 2Fgithub.com%2Fint-index%2Fghc-proposals%2Fblob%2Fvisible-forall
> | > > > > %2Fproposals%2F0000-visible-forall.rst&data=04%7C01%7Csimonp
> | > > > > j%40microsoft.com
> %7Ccba94a6d611e4700212608d88f87414e%7C72f988bf8
> | > > > > 6f141af91ab2d7cd011db47%7C1%7C1%7C637417159812849940%7CUnknown%7
> | > > > > CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWw
> | > > > > iLCJXVCI6Mn0%3D%7C3000&sdata=cfbyhbDYnPX%2BC7BKrak3mzPEFyiXY
> | > > > > wPhza3T1sv2X2I%3D&reserved=0
> | > > > >
> | > > > > While I suggested acceptance on the previous version, I am
> leaning
> | towards rejecting the proposal now. My reasoning is that I hadn't
> fully
> | understood all the aspects of the original proposal, and the new
> proposal
> | seems to lack a simple modular specification. There are *many* changes
> | described in the document, but I found it hard to understand what is
> the
> | current design, from the point of view of a user of the feature, as
> opposed
> | to someone trying to implement it.
> | > > > >
> | > > > > I'd be curious about what others think.
> | > > > >
> | > > > > -Iavor
> | > > > >
> | > > > >
> | > > > > _______________________________________________
> | > > > > ghc-steering-committee mailing list
> | > > > > ghc-steering-committee at haskell.org
> | > > > >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%
> | > > > > 2Fmail.haskell.org
> %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering
> | > > > > -committee&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d
> | > > > > 611e4700212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%
> | > > > > 7C1%7C637417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjA
> | > > > > wMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&s
> | > > > > data=JJjZfHZhOTQ6yo31ucKEFHC9hNIXG9McT18FbuYbgvI%3D&reserved
> | > > > > =0
> | > > > --
> | > > > Joachim Breitner
> | > > > mail at joachim-breitner.de
> | > > >
> | > > >
> https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fw
> | > > > ww.joachim-breitner.de
> %2F&data=04%7C01%7Csimonpj%40microsoft.c
> | > > > om%7Ccba94a6d611e4700212608d88f87414e%7C72f988bf86f141af91ab2d7cd0
> | > > > 11db47%7C1%7C1%7C637417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIj
> | > > > oiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C300
> | > > > 0&sdata=BArEbQSBvN4zsTDWtN9PW3klvk1c05lX8hhm2jMKk5E%3D&res
> | > > > erved=0
> | > > >
> | > > >
> | > > > _______________________________________________
> | > > > ghc-steering-committee mailing list
> | > > > ghc-steering-committee at haskell.org
> | > > >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2F
> | > > > mail.haskell.org
> %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-com
> | > > > mittee&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e47
> | > > > 00212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63
> | > > > 7417159812849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQI
> | > > > joiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=JJjZfHZ
> | > > > hOTQ6yo31ucKEFHC9hNIXG9McT18FbuYbgvI%3D&reserved=0
> | > >
> | > > _______________________________________________
> | > > ghc-steering-committee mailing list
> | > > ghc-steering-committee at haskell.org
> | > >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fma
> | > > il.haskell.org
> %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committ
> | > > ee&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e47002126
> | > > 08d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C6374171598
> | > > 12849940%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzI
> | > > iLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=JJjZfHZhOTQ6yo31ucK
> | > > EFHC9hNIXG9McT18FbuYbgvI%3D&reserved=0
> | >
> | > _______________________________________________
> | > ghc-steering-committee mailing list
> | > ghc-steering-committee at haskell.org
> | >
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail
> | > .haskell.org
> %2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-committee&a
> | > mp;data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e4700212608d88f
> | > 87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812859933
> | > %7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6I
> | > k1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=er3qe80%2BcqnIn3UIKfjuGu4VDwkH7
> | > jEosJqR45eKvn4%3D&reserved=0
> | --
> | Joachim Breitner
> | mail at joachim-breitner.de
> |
> |
> https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim
> | -
> | breitner.de%2F&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e4700
> |
> 212608d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C63741715981285
> |
> 9933%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1
> |
> haWwiLCJXVCI6Mn0%3D%7C3000&sdata=dyYFsh09gm4vxafb%2FRfa36jb8QT%2BBlHUtx1
> | OK6AMf%2BE%3D&reserved=0
> |
> |
> | _______________________________________________
> | ghc-steering-committee mailing list
> | ghc-steering-committee at haskell.org
> |
> https://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fmail.haske
> | ll.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-steering-
> | committee&data=04%7C01%7Csimonpj%40microsoft.com
> %7Ccba94a6d611e470021260
> |
> 8d88f87414e%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C637417159812859933%
> |
> 7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwi
> |
> LCJXVCI6Mn0%3D%7C3000&sdata=er3qe80%2BcqnIn3UIKfjuGu4VDwkH7jEosJqR45eKvn
> | 4%3D&reserved=0
> _______________________________________________
> 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/20201125/ec7b4e48/attachment-0001.html>
More information about the ghc-steering-committee
mailing list