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

[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 <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 <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://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 <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 <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 <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
> 

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