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

[Richard Eisenberg]

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> 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

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