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

[Roman Leshchinskiy]

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
> --
> Joachim Breitner
>   mail at joachim-breitner.de
>   http://www.joachim-breitner.de/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-steering-committee/attachments/20180809/b86b9248/attachment.html>