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

[Simon Peyton Jones]

I support the proposal, because it allows the programmer to say things that we want to be able to say.  Notably, given
	data T k (a :: k)
what is the kind of T?  Writing down that kind should be possible, and should tell you how to use it.  We can't say
 	T :: forall k. k -> *
because then we'd expect to be able to write (T Maybe), with the kind argument filled in implicitly.  We need some way to specify this when giving kind signatures.

I'm all for sketching the big picture, as a way to indicate that we aren't painting ourselves into a corner.   The table in one of the github comments is useful, and would be useful as a way to describe the landscape.

Really the only thing at issue is the syntax. In
   forall a -> blah
the thing on the left of the arrow isn't a type at all, unlike normal uses of arrow.  It's more like
   forall a. blah
   forall a% blah
that is, two related constructs with a syntactic signal about whether the argument is explicit or not.

On the whole I'm happy with the "->".  We are used to supplying arguments for things on the LHS of an arrow.

I'm not clear about abstraction...I'll put a question on the github trail.

Simon

|  -----Original Message-----
|  From: ghc-steering-committee [mailto:ghc-steering-committee-
|  bounces at haskell.org] On Behalf Of Roman Leshchinskiy
|  Sent: 20 December 2017 20:36
|  To: ghc-steering-committee at haskell.org
|  Subject: [ghc-steering-committee] Proposal: Syntax for visible dependent
|  quantification (#81)
|  
|  Hi everyone,
|  
|  The proposal is about adding support for dependent quantification to kind
|  signatures:
|  
|  
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%
|  2Fghc-proposals%2Fghc-
|  proposals%2Fpull%2F81&data=02%7C01%7Csimonpj%40microsoft.com%7Cf4bcb638ccb04
|  882991608d547e94370%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C63649398954
|  3774014&sdata=Zvjdonwoja%2FlKZ14CND4nxVZur8a4Um867wsvtZr6%2FQ%3D&reserved=0
|  
|  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://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.cis.upen
|  n.edu%2F~sweirich%2Fpapers%2Feisenberg-
|  thesis.pdf&data=02%7C01%7Csimonpj%40microsoft.com%7Cf4bcb638ccb04882991608d5
|  47e94370%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636493989543774014&sda
|  ta=1U0KSOBPJ5p%2Byr6dYNtmZmXF0rq%2BEls7CJFDCmCCRmA%3D&reserved=0).
|  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://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com
|  %2Fghc-proposals%2Fghc-proposals%2Fpull%2F81%23issuecomment-
|  336892922&data=02%7C01%7Csimonpj%40microsoft.com%7Cf4bcb638ccb04882991608d54
|  7e94370%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636493989543774014&sdat
|  a=kuDAxA3Tf1sKoA4CSllCp66sxvBo6nLMLQYCWBainzQ%3D&reserved=0).
|  
|  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