[ghc-steering-committee] Proposal: Syntax for visible dependent quantification (#81)

Sun Sep 30 17:46:58 UTC 2018

Hi,

guess we have consensus. Accepted.

Joachim

Am Freitag, den 17.08.2018, 11:19 +0000 schrieb Simon Peyton Jones via
ghc-steering-committee:
> I support this #81.
>  
> Simon
>  
> From: ghc-steering-committee <ghc-steering-committee-bounces at haskell.org> On Behalf Of Roman Leshchinskiy
> Sent: 09 August 2018 19:44
> To: Joachim Breitner <mail at joachim-breitner.de>
> Cc: ghc-steering-committee at haskell.org
> Subject: Re: [ghc-steering-committee] Proposal: Syntax for visible dependent quantification (#81)
>  
> Sorry for the long delay. Given that the general feedback is positive and #102 is now available, I recommend that we accept #81.
>  
> Thanks,
>  
> Roman
>  
> On Sat, May 5, 2018 at 10:12 PM, Joachim Breitner <mail at joachim-breitner.de> wrote:
> > Hi,
> > 
> > indeed, we should make progress here. Roman, with #102 discussed
> > (albeit not decided), what is your recommendation about #81?
> > 
> > Cheers,
> > Joachim
> > 
> > Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg:
> > > Hi committee,
> > > 
> > > 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.
> > > 
> > > Thanks!
> > > Richard
> > > 
> > > > On Jan 5, 2018, at 8:37 PM, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> > > > 
> > > > OK. I've posted proposal #102 (https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst) which describes the full set of quantifiers for Dependent Haskell.
> > > > 
> > > > I continue to think that #81 can stand alone, but those who want a larger picture can see #102 for that larger picture.
> > > > 
> > > > Thanks,
> > > > Richard
> > > > 
> > > > > On Dec 21, 2017, at 9:15 AM, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> > > > > 
> > > > > 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).
> > > > > 
> > > > > I'll put together yet another proposal. :)
> > > > > 
> > > > > 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.
> > > > > 
> > > > > Thanks,
> > > > > Richard
> > > > > 
> > > > > > On Dec 20, 2017, at 3:35 PM, Roman Leshchinskiy <rleshchinskiy at gmail.com> wrote:
> > > > > > 
> > > > > > Hi everyone,
> > > > > > 
> > > > > > The proposal is about adding support for dependent quantification to
> > > > > > kind signatures:
> > > > > > 
> > > > > > https://github.com/ghc-proposals/ghc-proposals/pull/81
> > > > > > 
> > > > > > Consider the following declaration (example lifted from the proposal):
> > > > > > 
> > > > > > data T k (a :: k)
> > > > > > 
> > > > > > GHC accepts this but it can't be given an explicit kind. Internally,
> > > > > > it is assigned a kind which is rendered as
> > > > > > 
> > > > > > forall k -> k -> *
> > > > > > 
> > > > > > but this isn't accepted in source code. Note that in applications of
> > > > > > T, k must be specified explicitly (e.g., T Type Int) which is why T
> > > > > > does *not* have the kind
> > > > > > 
> > > > > > forall k. k -> *
> > > > > > 
> > > > > > Moreover, k is mentioned later in the kind which is why something like
> > > > > > Type -> k -> * doesn't work, either.
> > > > > > 
> > > > > > The proposal is to allow forall k -> k -> * and similar kinds to
> > > > > > appear in source code.
> > > > > > 
> > > > > > This is actually intended as the first in a series of proposals
> > > > > > driving us towards dependent types in Haskell as described in
> > > > > > Richard's thesis
> > > > > > (https://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf).
> > > > > > Ultimately, the intention is to have all of the following (cf. Chapter
> > > > > > 4 of the thesis):
> > > > > > 
> > > > > > forall a. t
> > > > > > forall a -> t
> > > > > > pi a. t
> > > > > > pi a -> t
> > > > > > 
> > > > > > Here, forall and pi express relevance (does it exist at runtime) and .
> > > > > > and -> express visibility (does it have to be specified explicitly).
> > > > > > 
> > > > > > Because of this, my recommendation is to strongly encourage the author
> > > > > > to submit an extended proposal which reserves (but doesn't specify the
> > > > > > semantics of) the above syntax wholesale.
> > > > > > 
> > > > > > This would allow us to ensure that various bits of Dependent Haskell
> > > > > > use consistent syntax and language extensions once implemented. I find
> > > > > > it quite difficult to discuss just this specific bit of syntax in
> > > > > > isolation. Indeed, the public discussion was rather confused without
> > > > > > an explanation of the roadmap
> > > > > > (https://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-336892922).
> > > > > > 
> > > > > > Alternatively, we could just agree on the roadmap ourselves, without
> > > > > > public discussion. This would somewhat circumvent the process, though.
> > > > > > 
> > > > > > If we decide to discuss just the proposal as is, though, then I'd be
> > > > > > weakly against the proposed syntax as it is too subtle for my taste
> > > > > > and abuses familiar mathematical notation somewhat. I'd probably
> > > > > > prefer something like:
> > > > > > 
> > > > > > type a -> t
> > > > > > 
> > > > > > The proposal also doesn't specify what language extension would turn
> > > > > > on support for the syntax so this would have to be rectified.
> > > > > > 
> > > > > > Thanks,
> > > > > > 
> > > > > > Roman
> > > > > > _______________________________________________
> > > > > > ghc-steering-committee mailing list
> > > > > > ghc-steering-committee at haskell.org
> > > > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > > > > 
> > > > > _______________________________________________
> > > > > ghc-steering-committee mailing list
> > > > > ghc-steering-committee at haskell.org
> > > > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > > 
> > > _______________________________________________
> > > ghc-steering-committee mailing list
> > > ghc-steering-committee at haskell.org
> > > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
> > _______________________________________________
> > ghc-steering-committee mailing list
> > ghc-steering-committee at haskell.org
> > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180930/892b7a55/attachment.sig>