Proposal: Syntax for visible dependent quantification (#81)

Roman Leshchinskiy

20 Dec 2017 20 Dec '17

3:35 p.m.

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

Show replies by date

Simon Peyton Jones

21 Dec 21 Dec

7:09 a.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

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@haskell.org] On Behalf Of Roman Leshchinskiy | Sent: 20 December 2017 20:36 | To: ghc-steering-committee@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@haskell.org | https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Richard Eisenberg

9:15 a.m.

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

Richard Eisenberg

5 Jan 5 Jan

8:37 p.m.

New subject: 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

Richard Eisenberg

15 Apr 15 Apr

11:09 p.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

Hi committee, I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by. Thanks! Richard

...

On Jan 5, 2018, at 8:37 PM, Richard Eisenberg wrote:

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 mailto:rae@cs.brynmawr.edu> 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 mailto: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 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 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... 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 mailto: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 mailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

Joachim Breitner

5 May 5 May

5:12 p.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

Hi, indeed, we should make progress here. Roman, with #102 discussed (albeit not decided), what is your recommendation about #81? Cheers, Joachim Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg:

...

Hi committee,

I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by.

Thanks! Richard

...
On Jan 5, 2018, at 8:37 PM, Richard Eisenberg wrote:

OK. I've posted proposal #102 (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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Roman Leshchinskiy

9 Aug 9 Aug

2:44 p.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

Sorry for the long delay. Given that the general feedback is positive and #102 is now available, I recommend that we accept #81. Thanks, Roman On Sat, May 5, 2018 at 10:12 PM, Joachim Breitner wrote:

...

Hi,

indeed, we should make progress here. Roman, with #102 discussed (albeit not decided), what is your recommendation about #81?

Cheers, Joachim

...
Hi committee,

I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by.

Thanks! Richard

...
On Jan 5, 2018, at 8:37 PM, Richard Eisenberg wrote:

OK. I've posted proposal #102 (https://github.com/ goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst) which describes

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

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

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

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

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

...
...
...
...
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,

Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg: the full set of quantifiers for Dependent Haskell. 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). the proposed syntax is a little subtle. proposal): like the 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

_______________________________________________ ghc-steering-committee mailing list ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Simon Peyton Jones

17 Aug 17 Aug

7:19 a.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

I support this #81. Simon From: ghc-steering-committee On Behalf Of Roman Leshchinskiy Sent: 09 August 2018 19:44 To: Joachim Breitner Cc: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Proposal: Syntax for visible dependent quantification (#81) Sorry for the long delay. Given that the general feedback is positive and #102 is now available, I recommend that we accept #81. Thanks, Roman On Sat, May 5, 2018 at 10:12 PM, Joachim Breitner mailto:mail@joachim-breitner.de> wrote: Hi, indeed, we should make progress here. Roman, with #102 discussed (albeit not decided), what is your recommendation about #81? Cheers, Joachim Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg:

...

Hi committee,

I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by.

Thanks! Richard

...
On Jan 5, 2018, at 8:37 PM, Richard Eisenberg mailto:rae@cs.brynmawr.edu> wrote:

OK. I've posted proposal #102 (https://github.com/goldfirere/ghc-proposals/blob/pi/proposals/0000-pi.rst https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fgoldfirere%2Fghc-proposals%2Fblob%2Fpi%2Fproposals%2F0000-pi.rst&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599807360&sdata=lieSdDGUo7Pts%2F%2FIaWKAHPXnMF8OseDu5GGyy0iMYo8%3D&reserved=0) 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 mailto:rae@cs.brynmawr.edu> 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 mailto: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 https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%2Fpull%2F81&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599807360&sdata=VAlKyMTnw%2BywQ46AEhOgAhEsRLU7TagmS9Winqjwnlw%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://www.cis.upenn.edu/~sweirich/papers/eisenberg-thesis.pdf https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fwww.cis.upenn.edu%2F~sweirich%2Fpapers%2Feisenberg-thesis.pdf&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C1%7C636694370599817364&sdata=b3y9GWTM8Q0DbYxtx4XspKx%2BrR1qbCYbdtRj%2BSjONdY%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://github.com/ghc-proposals/ghc-proposals/pull/81#issuecomment-33689292...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%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599817364&sdata=%2Ft0UNHhKAyPJRDifK1q31Fpc2LNWfuTyl3PCUIHourI%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@haskell.orgmailto: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.orgmailto: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.orgmailto:ghc-steering-committee@haskell.org https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee -- Joachim Breitner mail@joachim-breitner.demailto:mail@joachim-breitner.de http://www.joachim-breitner.de/https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim-breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C3ccaf4dae6074e10d27808d5fe281cef%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636694370599827378&sdata=mE%2FLHhl4iswq84Ol1QPDJ5DITtya6jahvEiWpE%2BbZwE%3D&reserved=0

Joachim Breitner

30 Sep 30 Sep

1:46 p.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

Hi, guess we have consensus. Accepted. Joachim Am Freitag, den 17.08.2018, 11:19 +0000 schrieb Simon Peyton Jones via ghc-steering-committee:

...

I support this #81.

Simon

From: ghc-steering-committee On Behalf Of Roman Leshchinskiy Sent: 09 August 2018 19:44 To: Joachim Breitner Cc: ghc-steering-committee@haskell.org Subject: Re: [ghc-steering-committee] Proposal: Syntax for visible dependent quantification (#81)

Sorry for the long delay. Given that the general feedback is positive and #102 is now available, I recommend that we accept #81.

Thanks,

Roman

On Sat, May 5, 2018 at 10:12 PM, Joachim Breitner wrote:

...
Hi,

indeed, we should make progress here. Roman, with #102 discussed (albeit not decided), what is your recommendation about #81?

Cheers, Joachim

Am Sonntag, den 15.04.2018, 23:09 -0400 schrieb Richard Eisenberg:

...
Hi committee,

I'd like to reboot this discussion, now that #102 has been written, debated, and tabled. As a reminder, this proposal is blocking #54, which will cure real bugs GHC is plagued by.

Thanks! Richard

...
On Jan 5, 2018, at 8:37 PM, Richard Eisenberg wrote:

OK. I've posted proposal #102 (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

_______________________________________________ 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 -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

Joachim Breitner

5 Jan 5 Jan

3:55 p.m.

New subject: Proposal: Syntax for visible dependent quantification (#81)

Hi, thanks for the recommendation. Am Mittwoch, den 20.12.2017, 20:35 +0000 schrieb Roman Leshchinskiy:

...

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

I am not saying that the proposed “forall a ->” syntax is great, but I think it is still better than “type a -> …”. The reason is that we already use prefixing “type”, e.g. in export lists (“type Bool”), to say “this thing is a type” if there is ambiguity. So if anything, then ifThenElse :: Bool -> a -> a -> a should be also allowed to be written as ifThenElse :: type Bool -> a -> a -> a and hence, in consequence ifThenElse :: type Bool -> type a -> type a -> a In other words, “type foo” just clarifies “I mean the _type_ foo”. Can we get more input?

...

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.

I’d be on board deciding on that syntax all in one go. Joachim -- Joachim Breitner mail@joachim-breitner.de http://www.joachim-breitner.de/

2424

Age (days ago)

2708

Last active (days ago)

List overview

Download

9 comments

4 participants

participants (4)

Joachim Breitner
Richard Eisenberg
Roman Leshchinskiy
Simon Peyton Jones