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

Sat May 5 21:12:33 UTC 2018

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
-- 
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/20180505/00a40a88/attachment-0001.sig>