<div dir="ltr">Sorry for the long delay. Given that the general feedback is positive and #102 is now available, I recommend that we accept #81.<div><br></div><div>Thanks,</div><div><br></div><div>Roman</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 5, 2018 at 10:12 PM, Joachim Breitner <span dir="ltr"><<a href="mailto:mail@joachim-breitner.de" target="_blank">mail@joachim-breitner.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
indeed, we should make progress here. Roman, with #102 discussed<br>
(albeit not decided), what is your recommendation about #81?<br>
<br>
Cheers,<br>
Joachim<br>
<div class="HOEnZb"><div class="h5"><br>
Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg:<br>
> Hi committee,<br>
> <br>
> I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by.<br>
> <br>
> Thanks!<br>
> Richard<br>
> <br>
> > On Jan 5, 2018, at 8:37 PM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br>
> > <br>
> > OK. I've posted proposal #102 (<a href="https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst" rel="noreferrer" target="_blank">https://github.com/<wbr>goldfirere/ghc-proposals/blob/<wbr>pi/proposals/0000-pi.rst</a>) which describes the full set of quantifiers for Dependent Haskell.<br>
> > <br>
> > I continue to think that #81 can stand alone, but those who want a larger picture can see #102 for that larger picture.<br>
> > <br>
> > Thanks,<br>
> > Richard<br>
> > <br>
> > > On Dec 21, 2017, at 9:15 AM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu">rae@cs.brynmawr.edu</a>> wrote:<br>
> > > <br>
> > > These are good suggestions. Thanks. While I'm writing all these proposals, it's about time I introduce pi proper -- the proposal for pi can go further than reserve syntax, because there are already places in the language that support real pi-types (the kinds of type families [assuming #54 is accepted] and the kinds of datatypes).<br>
> > > <br>
> > > I'll put together yet another proposal. :)<br>
> > > <br>
> > > Regardless, I don't want to shut down debate on this proposal in isolation. In particular, I'd love new syntax suggestions, as I agree that the proposed syntax is a little subtle.<br>
> > > <br>
> > > Thanks,<br>
> > > Richard<br>
> > > <br>
> > > > On Dec 20, 2017, at 3:35 PM, Roman Leshchinskiy <<a href="mailto:rleshchinskiy@gmail.com">rleshchinskiy@gmail.com</a>> wrote:<br>
> > > > <br>
> > > > Hi everyone,<br>
> > > > <br>
> > > > The proposal is about adding support for dependent quantification to<br>
> > > > kind signatures:<br>
> > > > <br>
> > > > <a href="https://github.com/ghc-proposals/ghc-proposals/pull/81" rel="noreferrer" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals/pull/<wbr>81</a><br>
> > > > <br>
> > > > Consider the following declaration (example lifted from the proposal):<br>
> > > > <br>
> > > > data T k (a :: k)<br>
> > > > <br>
> > > > GHC accepts this but it can't be given an explicit kind. Internally,<br>
> > > > it is assigned a kind which is rendered as<br>
> > > > <br>
> > > > forall k -> k -> *<br>
> > > > <br>
> > > > but this isn't accepted in source code. Note that in applications of<br>
> > > > T, k must be specified explicitly (e.g., T Type Int) which is why T<br>
> > > > does *not* have the kind<br>
> > > > <br>
> > > > forall k. k -> *<br>
> > > > <br>
> > > > Moreover, k is mentioned later in the kind which is why something like<br>
> > > > Type -> k -> * doesn't work, either.<br>
> > > > <br>
> > > > The proposal is to allow forall k -> k -> * and similar kinds to<br>
> > > > appear in source code.<br>
> > > > <br>
> > > > This is actually intended as the first in a series of proposals<br>
> > > > driving us towards dependent types in Haskell as described in<br>
> > > > Richard's thesis<br>
> > > > (<a href="https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf" rel="noreferrer" target="_blank">https://www.cis.upenn.edu/~<wbr>sweirich/papers/eisenberg-<wbr>thesis.pdf</a>).<br>
> > > > Ultimately, the intention is to have all of the following (cf. Chapter<br>
> > > > 4 of the thesis):<br>
> > > > <br>
> > > > forall a. t<br>
> > > > forall a -> t<br>
> > > > pi a. t<br>
> > > > pi a -> t<br>
> > > > <br>
> > > > Here, forall and pi express relevance (does it exist at runtime) and .<br>
> > > > and -> express visibility (does it have to be specified explicitly).<br>
> > > > <br>
> > > > Because of this, my recommendation is to strongly encourage the author<br>
> > > > to submit an extended proposal which reserves (but doesn't specify the<br>
> > > > semantics of) the above syntax wholesale.<br>
> > > > <br>
> > > > This would allow us to ensure that various bits of Dependent Haskell<br>
> > > > use consistent syntax and language extensions once implemented. I find<br>
> > > > it quite difficult to discuss just this specific bit of syntax in<br>
> > > > isolation. Indeed, the public discussion was rather confused without<br>
> > > > an explanation of the roadmap<br>
> > > > (<a href="https://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-336892922" rel="noreferrer" target="_blank">https://github.com/ghc-<wbr>proposals/ghc-proposals/pull/<wbr>81#issuecomment-336892922</a>).<br>
> > > > <br>
> > > > Alternatively, we could just agree on the roadmap ourselves, without<br>
> > > > public discussion. This would somewhat circumvent the process, though.<br>
> > > > <br>
> > > > If we decide to discuss just the proposal as is, though, then I'd be<br>
> > > > weakly against the proposed syntax as it is too subtle for my taste<br>
> > > > and abuses familiar mathematical notation somewhat. I'd probably<br>
> > > > prefer something like:<br>
> > > > <br>
> > > > type a -> t<br>
> > > > <br>
> > > > The proposal also doesn't specify what language extension would turn<br>
> > > > on support for the syntax so this would have to be rectified.<br>
> > > > <br>
> > > > Thanks,<br>
> > > > <br>
> > > > Roman<br>
> > > > ______________________________<wbr>_________________<br>
> > > > ghc-steering-committee mailing list<br>
> > > > <a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@<wbr>haskell.org</a><br>
> > > > <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-<wbr>steering-committee</a><br>
> > > <br>
> > > ______________________________<wbr>_________________<br>
> > > ghc-steering-committee mailing list<br>
> > > <a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@<wbr>haskell.org</a><br>
> > > <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-<wbr>steering-committee</a><br>
> <br>
> ______________________________<wbr>_________________<br>
> ghc-steering-committee mailing list<br>
> <a href="mailto:ghc-steering-committee@haskell.org">ghc-steering-committee@<wbr>haskell.org</a><br>
> <a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" rel="noreferrer" target="_blank">https://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-<wbr>steering-committee</a><br>
</div></div><div class="HOEnZb"><div class="h5">-- <br>
Joachim Breitner<br>
  <a href="mailto:mail@joachim-breitner.de">mail@joachim-breitner.de</a><br>
  <a href="http://www.joachim-breitner.de/" rel="noreferrer" target="_blank">http://www.joachim-breitner.<wbr>de/</a><br>
</div></div></blockquote></div><br></div>