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

[Roman Leshchinskiy]

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