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

[Richard Eisenberg]

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