[ghc-steering-committee] DH quantifiers (#102), Recommendation: accept

[Simon Peyton Jones]

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 at haskell.org] On Behalf Of Joachim Breitner
|  Sent: 23 February 2018 15:39
|  To: ghc-steering-committee at 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 at 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