Why do we need this now? There's lots of new syntax. Is it solving tomorrow's problems, or todays? Does the proposal subsume #81 (syntax for visible dependent quantification)? That one /does/ have a current motivation. Perhaps #102 is just a grander version of #81, reserving the syntax but with #81 as the sole current motivation? I'm very to get #81 nailed, because #54 depends on it, and #54 is highly desirable. Simon | -----Original Message----- | From: ghc-steering-committee [mailto:ghc-steering-committee- | bounces@haskell.org] On Behalf Of Joachim Breitner | Sent: 23 February 2018 15:39 | To: ghc-steering-committee@haskell.org | Subject: [ghc-steering-committee] DH quantifiers (#102), | Recommendation: accept | | Dear Committee, | | this is your secretary speaking: | | Dependent Haskell quantifiers were proposed, by Richard. | https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithu | b.com%2Fghc-proposals%2Fghc- | proposals%2Fpull%2F102&data=04%7C01%7Csimonpj%40microsoft.com%7Cae897a | 251ef548cae01208d57ad39830%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0% | 7C636549971570003501%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQI | joiV2luMzIiLCJBTiI6Ik1haWwifQ%3D%3D%7C- | 1&sdata=28T40QgHYUtkWDOMlME%2B9oj4HNf0d51pyb6i5901kLY%3D&reserved=0 | rendered at | https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithu | b.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fpi%2Fproposals%2F0000- | pi.rst&data=04%7C01%7Csimonpj%40microsoft.com%7Cae897a251ef548cae01208 | d57ad39830%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63654997157000 | 3501%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBT | iI6Ik1haWwifQ%3D%3D%7C- | 1&sdata=FLdmQUBlj57sKoREiOqDGXP%2B%2Bw98j3nZG5Z0uZy6wnA%3D&reserved=0 | | I’ll shepherd that myself. | | This proposal defines and reserves the syntax for the quantifiers that | eventually Dependent Haskell will need, and allows their use where it | makes sense already (e.g. in Kinds). The quantifier are: | | forall a. | forall a '. | forall a -> | forall a '-> | foreach a. | foreach a '. | foreach a -> | foreach a '-> | ty => | ty '=> | ty -> | ty '-> | | | It addresses the interaction with warning (e.g. -Wcompat). It looks | well-thought-through, one might infer that the authors wrote a thesis | about this stuff. | | There is some syntactic bikeshedding possible; for example the | proposal proposes "foreach" instead of "pi" (the latter would make | "pi" a keyword, which would be unfortunate for those who deal with | circles). | | If someone has better ideas, in particular about the use of ' to | denote matchable arrows, we still have time to suggest them. | | I recommend to accept this proposal in the current form or with | further refinements to the syntax, if we can come up with them. | | | Thanks, | Joachim | -- | Joachim Breitner | mail@joachim-breitner.de | | https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.jo | achim- | breitner.de%2F&data=04%7C01%7Csimonpj%40microsoft.com%7Cae897a251ef548 | cae01208d57ad39830%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636549 | 971570003501%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luM | zIiLCJBTiI6Ik1haWwifQ%3D%3D%7C- | 1&sdata=tH%2Fxbrv4JFzFpoJ3rUm3Nz5GY7ULs1VYFRLXvvYrD5U%3D&reserved=0