April 2018 - ghc-steering-committee

Proposal: Syntax for visible dependent quantification (#81)
by Roman Leshchinskiy 01 Oct '18

01 Oct '18

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-3368929…) 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

4 9

Proposal: Binding existential type variables (#96)
by Roman Leshchinskiy 24 Jun '18

24 Jun '18

Hi everyone, The proposal is to add a way to name existential type variables in pattern matches: https://github.com/ghc-proposals/ghc-proposals/pull/96. Suppose we have a constructor with an existential: data T where MkT :: forall a. Show a => a -> T Under the proposal, we could then bind that existential in a match against MkT: f :: T -> String f (MkT @a x) = show (x :: a) Note that this reuses the syntax for visible type application. Only the forms @a (where 'a' is a variable) and @_ are permitted. In the discussion the following major questions have been raised. 1. What about universally quantified type variables, such as 'a' in the following definition: data U a where MkU :: forall a b. Show a => b -> T a Do we need to mention 'a' in a pattern match against MkU? The answer (now reflected in the proposal) is no - universally quantified type variables can't be bound in this way. The pattern would look like this: g :: U a -> String g (MkU @b x) = show (x :: b) The bulk of the discussion was about this question. 2. What exactly is an existential? The above examples are clear but what about: type family Id a where Id a = a data T a where MkT :: forall a. a -> T (Id a) This is an existential under the current rules but given this, the distinction between existentials and universals might be not entirely intuitive. 3. What about pattern synonyms? The proposal now clarifies that they are treated exactly the same as data constructors. My recommendation is to reject the proposal as is but to encourage the authors to come up with a different syntax. The reason is that the proposal "steals" the syntax for explicit type application in patterns but it seems to me that type application in patterns makes perfect sense! I don't see why I shouldn't be eventually able to write something like: data C a = C a h (C @Int n) = n and have the compiler infer h :: C Int -> Int. Having @type mean something other than type application in pattern seems highly confusing to me and kills a possibly useful future feature. I believe a lot of the confusion with respect to point 1 above happened precisely because the proposal blurs the difference between type application and binding in patterns. As to syntax, perhaps using 'type' or 'forall' as type binders instead of '@' would work. Thanks, Roman

5 6

Proposal: Or patterns (#43)
by Manuel M T Chakravarty 19 Jun '18

19 Jun '18

Folks, I am sorry for taking a long time to get us going on this proposal. The ”Or pattern” proposal is about an extension to pattern matching: (formatted) https://github.com/osa1/ghc-proposals/blob/or_patterns/proposals/0000-or-pa… (PR thread) https://github.com/ghc-proposals/ghc-proposals/pull/43 Its basic idea is simple: allow multiple alternative patterns for each alternative during pattern matching. Unfortunately, the interaction with guards and some other languages features makes it significantly less straight forward than one might initially think. I propose to accept this proposal provided we can agree to use the ”first semantics” (aka single-match semantics) — see https://github.com/osa1/ghc-proposals/blob/or_patterns/proposals/0000-or-pa… My reason for insisting on the first semantics is that it is a simple extension of the existing pattern semantics in the Report, whereas the second semantics requires a more profound, non-local change. This, in particular, also makes it easier to understand the implications of the first semantics. (Also, OCaml has made that same choice.) However, even with the first semantics, I still have one concern about this proposal. The story about the interaction with existential types is currently only partial and there is no discussion of the interaction with GADTs. It might be reasonable to ask for a complete specification of the interaction with these features before making a final determination on this proposal. Nevertheless, this proposal is quite elaborate and quite some work has gone into it. Hence, I think, we owe it the authors of the proposal to at least make a preliminary determination at this point. (In particular, if it is not going to fly regardless of how GADTs are handled, we should say so now.) Cheers, Manuel PS: It is worth noting that Swift solved the problem of deciding between the first and second semantics by choosing a syntax that avoids the ambiguity: <https://developer.apple.com/library/content/documentation/Swift/Conceptual/…>. It is difficult to adapt this syntax to Haskell. If it where possible, I think, this would be the best solution.

6 14

Treat kind and type vars identically with `forall` #103
by Simon Peyton Jones 23 May '18

23 May '18

Dear GHC steering committee I strongly propose that we accept Treat kind and type vars identically with `forall` #103 https://github.com/ghc-proposals/ghc-proposals/pull/103 It makes our design much more simple and uniform - both in the specification and in the implementation. The current setup is a terrible dogs breakfast. Moreover, I propose that we adopt it without a 3-release wait after #83 - see under Alternatives. Any programs that are rejected by #103 can be fixed by adding some extra forall k's. And that change will be accepted NOW if you add -XTypeInType. Simon

4 7

Deriving via (#120), Recommendation: accept
by Joachim Breitner 22 May '18

22 May '18

Dear Committee, this is your secretary speaking: Deriving via was proposed, by Ryan, Icelandjack and Andres, https://github.com/ghc-proposals/ghc-proposals/pull/120 rendered at https://github.com/Icelandjack/ghc-proposals/blob/patch-3/proposals/0000-de… I’ll shepherd that myself. The proposal adds a new deriving strategy that works like GND, but explicitly names the other, representationally equal type whose instance should be copied. The proposal comes with a paper and an implementation, has been met with great enthusiasm in the community, and I expect that our users will do many great things with it, and all that with relatively little theoretical and implemntational overhead. I therefore wholeheartedly recomment that we accept this proposal. Thanks, Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

3 4

Please review: Mutable constructor fields, Shepherd: Ryan Newton
by Joachim Breitner 08 May '18

08 May '18

Dear Committee, this is your secretary speaking: https://github.com/ghc-proposals/ghc-proposals/pull/8 was brought before the committee, by our own Simon Marlow. I propose Ryan Newton as the Shepherd, because he asked for it :-) Ryan, please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you. Greetings, Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

7 18

Please Review: Kinds Without Promotion, Shepherd: Ryan Newton
by Joachim Breitner 06 May '18

06 May '18

Dear Committee, this is your secretary speaking: Kinds Without Promotion by Yavor https://github.com/ghc-proposals/ghc-proposals/pull/106 I propose Ryan Newton as the shepherd. Ryan, please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you. Thanks, Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

1 1

Please Review: Top-level kind signatures, Shepherd: Roman Leshchinskiy
by Joachim Breitner 06 May '18

06 May '18

Dear Committee, this is your secretary speaking: Top-level kind signatures by Richard has been proposed: https://github.com/ghc-proposals/ghc-proposals/pull/54 I propose Roman Leshchinskiy as the shepherd, who is already shepherding the closely related proposal #81. Roman, please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you. Thanks, -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

1 1

Committee Discussion : Lazy unboxed tuples
by Ryan Newton 06 May '18

06 May '18

Dear Committee, The public discussion <https://github.com/ghc-proposals/ghc-proposals/pull/35> for this one <https://github.com/goldfirere/ghc-proposals/blob/unbanged-strict-patterns/p…> has happened, now for 4 weeks of committee discussion and final accept/reject. In that public discussion, you can see on Jan 11 options broken down as (1),(2),(3), with this proposal being (1). This seems to have stopped in a weird place where there was some substantial argument for (2) and (3) in the latter half of the comments, but the proposal is for (1). Richard, one bit that threw me off was this: *"we should require the bang even on bare variables, but that would break a lot of code I think."* Because that makes it seem like in spite of this cleaning-up proposal, GHC still has a basically inconsistent position on how to interpret variable-bindings of unlifted kind in patterns. Discuss? -Ryan On Tue, Jul 11, 2017 at 11:08 AM, Joachim Breitner <mail(a)joachim-breitner.de > wrote: > Hi, > > it is by Richard, I just got the URL wrong. The right pull request is > https://github.com/ghc-proposals/ghc-proposals/pull/35 > sorry for that. > > Using this thread is fine. > > Joachim > > Am Dienstag, den 11.07.2017, 10:58 -0400 schrieb Ryan Newton: > > Just to clarify, this is proposed by a user "winterland". I.e. not > > Richard, right? In the process document it is the author that "brings > > it before the committee" correct? > > > > I checked and it looks like our process document does not specify the > > means of our committee discussion. I propose we discuss this one > > right here on this thread, which we've already got sitting in our > > inboxes. > > > > Best, > > -Ryan > > > > > > On Tue, Jul 11, 2017 at 2:58 AM, Joachim Breitner <mail@joachim-breit > > ner.de> wrote: > > > Dear Committee, > > > > > > this is your secretary speaking: > > > > > > https://github.com/ghc-proposals/ghc-proposals/pull/45 > > > was brought before the committee, by our own Richard. > > > > > > I propose Ryan Newton as the Shepherd, just to rotate this role > > > properly. > > > > > > Ryan, please reach consensus as described in > > > https://github.com/ghc-proposals/ghc-proposals#committee-process > > > > > > I suggest you make a recommendation about the decision, maybe point > > > out > > > debatable points, and assume that anyone who stays quiet agrees > > > with > > > you. > > > > > > > > > Greetings, > > > Joachim > > > > > > > > > -- > > > Joachim Breitner > > > mail(a)joachim-breitner.de > > > http://www.joachim-breitner.de/ > > > > > > > > -- > Joachim “nomeata” Breitner > mail(a)joachim-breitner.de • https://www.joachim-breitner.de/ > XMPP: nomeata(a)joachim-breitner.de • OpenPGP-Key: 0xF0FBF51F > Debian Developer: nomeata(a)debian.org > _______________________________________________ > ghc-steering-committee mailing list > ghc-steering-committee(a)haskell.org > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee > >

5 6

Please Review: ExtraCommas (#87), Shepherd: Chris Allen
by Joachim Breitner 01 May '18

01 May '18

Dear Committee, this is your secretary speaking: ExtraCommas has been proposed by Andrew Martin: https://github.com/ghc-proposals/ghc-proposals/pull/112 I propose Chris Allen as the shepherd. Chris, please reach consensus as described in https://github.com/ghc-proposals/ghc-proposals#committee-process I suggest you make a recommendation, in a new e-mail thread with the proposal number in the subject, about the decision, maybe point out debatable points, and assume that anyone who stays quiet agrees with you. Thanks, -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

3 2