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@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@haskell.org
https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee
_______________________________________________
ghc-steering-committee mailing list
ghc-steering-committee@haskell.orghttps://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee