<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><div class="">OK. I've posted proposal #102 (<a href="https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst" class="">https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst</a>) which describes the full set of quantifiers for Dependent Haskell.</div><div class=""><br class=""></div><div class="">I continue to think that #81 can stand alone, but those who want a larger picture can see #102 for that larger picture.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Richard</div><div><br class=""><blockquote type="cite" class=""><div class="">On Dec 21, 2017, at 9:15 AM, Richard Eisenberg <<a href="mailto:rae@cs.brynmawr.edu" class="">rae@cs.brynmawr.edu</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">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 class=""><br class="">I'll put together yet another proposal. :)<br class=""><br class="">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 class=""><br class="">Thanks,<br class="">Richard<br class=""><br class=""><blockquote type="cite" class="">On Dec 20, 2017, at 3:35 PM, Roman Leshchinskiy <<a href="mailto:rleshchinskiy@gmail.com" class="">rleshchinskiy@gmail.com</a>> wrote:<br class=""><br class="">Hi everyone,<br class=""><br class="">The proposal is about adding support for dependent quantification to<br class="">kind signatures:<br class=""><br class=""> <a href="https://github.com/ghc-proposals/ghc-proposals/pull/81" class="">https://github.com/ghc-proposals/ghc-proposals/pull/81</a><br class=""><br class="">Consider the following declaration (example lifted from the proposal):<br class=""><br class=""> data T k (a :: k)<br class=""><br class="">GHC accepts this but it can't be given an explicit kind. Internally,<br class="">it is assigned a kind which is rendered as<br class=""><br class=""> forall k -> k -> *<br class=""><br class="">but this isn't accepted in source code. Note that in applications of<br class="">T, k must be specified explicitly (e.g., T Type Int) which is why T<br class="">does *not* have the kind<br class=""><br class=""> forall k. k -> *<br class=""><br class="">Moreover, k is mentioned later in the kind which is why something like<br class="">Type -> k -> * doesn't work, either.<br class=""><br class="">The proposal is to allow forall k -> k -> * and similar kinds to<br class="">appear in source code.<br class=""><br class="">This is actually intended as the first in a series of proposals<br class="">driving us towards dependent types in Haskell as described in<br class="">Richard's thesis<br class="">(<a href="https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf" class="">https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf</a>).<br class="">Ultimately, the intention is to have all of the following (cf. Chapter<br class="">4 of the thesis):<br class=""><br class=""> forall a. t<br class=""> forall a -> t<br class=""> pi a. t<br class=""> pi a -> t<br class=""><br class="">Here, forall and pi express relevance (does it exist at runtime) and .<br class="">and -> express visibility (does it have to be specified explicitly).<br class=""><br class="">Because of this, my recommendation is to strongly encourage the author<br class="">to submit an extended proposal which reserves (but doesn't specify the<br class="">semantics of) the above syntax wholesale.<br class=""><br class="">This would allow us to ensure that various bits of Dependent Haskell<br class="">use consistent syntax and language extensions once implemented. I find<br class="">it quite difficult to discuss just this specific bit of syntax in<br class="">isolation. Indeed, the public discussion was rather confused without<br class="">an explanation of the roadmap<br class="">(<a href="https://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-336892922" class="">https://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-336892922</a>).<br class=""><br class="">Alternatively, we could just agree on the roadmap ourselves, without<br class="">public discussion. This would somewhat circumvent the process, though.<br class=""><br class="">If we decide to discuss just the proposal as is, though, then I'd be<br class="">weakly against the proposed syntax as it is too subtle for my taste<br class="">and abuses familiar mathematical notation somewhat. I'd probably<br class="">prefer something like:<br class=""><br class=""> type a -> t<br class=""><br class="">The proposal also doesn't specify what language extension would turn<br class="">on support for the syntax so this would have to be rectified.<br class=""><br class="">Thanks,<br class=""><br class="">Roman<br class="">_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></blockquote><br class="">_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></div></div></blockquote></div><br class=""></body></html>