Hi, Am Freitag, den 23.02.2018, 15:52 +0000 schrieb 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?
when #81 was proposed, Roman (as the shepherd) complained that on its own, the choice of syntax in #81 was not very well motivated just by that proposal. Maybe, if #81 was all there is to do, we’d choose a different syntax! So really, the syntax in #81 is motivated by coming up with a consistent and comprehensive syntax scheme for _all_ variations of the quantifier, and Roman asked Richard to write that up as one proposal, instead of introducing the syntax piece by piece. And that’s now #102. Cheers, Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/