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

Fri Aug 17 11:19:40 UTC 2018

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<mailto: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<mailto:rae at cs.brynmawr.edu>> wrote:
> >
> > OK. I've posted proposal #102 (https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fpi%2Fproposals%2F0000-pi.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599807360&sdata=lieSdDGUo7Pts%2F%2FIaWKAHPXnMF8OseDu5GGyy0iMYo8%3D&reserved=0>) 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<mailto: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<mailto: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<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F81&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599807360&sdata=VAlKyMTnw%2BywQ46AEhOgAhEsRLU7TagmS9Winqjwnlw%3D&reserved=0>
> > > >
> > > > 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<https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.cis.upenn.edu%2F~sweirich%2Fpapers%2Feisenberg-thesis.pdf&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636694370599817364&sdata=b3y9GWTM8Q0DbYxtx4XspKx%2BrR1qbCYbdtRj%2BSjONdY%3D&reserved=0>).
> > > > 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<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F81%23issuecomment-336892922&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599817364&sdata=%2Ft0UNHhKAyPJRDifK1q31Fpc2LNWfuTyl3PCUIHourI%3D&reserved=0>).
> > > >
> > > > 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<mailto: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<mailto: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<mailto:ghc-steering-committee at haskell.org>
> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
--
Joachim Breitner
  mail at joachim-breitner.de<mailto:mail at joachim-breitner.de>
  http://www.joachim-breitner.de/<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599827378&sdata=mE%2FLHhl4iswq84Ol1QPDJ5DITtya6jahvEiWpE%2BbZwE%3D&reserved=0>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180817/ccb86428/attachment-0001.html>