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

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 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 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-33689292...).

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