June 2018 - ghc-steering-committee

Bundling patterns with type synonyms (#28)
by Christopher Allen 27 Jan '19

27 Jan '19

The proposal I'm reviewing is: Bundling patterns with type synonyms by Bertram Felgenhauer and Joe Hermaszewski https://github.com/ghc-proposals/ghc-proposals/pull/28 Having reviewed the proposal and gone through some of the GHC Trac history, I think we should accept this proposal. There are a couple of open questions, ambiguities, and potential downsides but the overall complexity of the proposal doesn't cause me great concern. Cheers, Chris Allen

5 11

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

Extra Commas (#87), Recommend: accept
by Christopher Allen 06 Aug '18

06 Aug '18

https://github.com/ghc-proposals/ghc-proposals/pull/87 With the provisos mentioned by Simon starting here in mind: https://github.com/ghc-proposals/ghc-proposals/pull/87#issuecomment-3855365… I recommend we accept the proposal with the understanding that the final specification or implementation could be handled by GHC's code review process. I also have a concern about the potential interactions with TupleSections. If no objections are raised, it should be assumed that no one opposes this proposal. --- Chris Allen

7 14

Deprecating Exports (#134); Recommendation: accept
by Joachim Breitner 15 Jul '18

15 Jul '18

Hi, alanasp has proposed a Deprecating Exports mechanism: https://github.com/alanasp/ghc-proposals/blob/patch-2/proposals/deprecating… The gist is explained by this: module Data.List ( ... {-# DEPRECATE lines "Exported from Data.String instead" #-} , lines ...t ) where i.e. DEPRECATE pragmas in export lists cause warning when some other module uses the deprecated symbol when it is imported (only) via some deprecated export. This is a GSOC 2018 project, mentored by Matthew Pickering and Erik de Castro Lopo. The feature has a clear use-case, is self-contained and David Feuer (the containers maintainer) has already confirmed that there is a real demand for this. I suggest acceptance! As always, I will understand silence as tactic consensus. Cheers, Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

4 9

Remove TypeOperators => NoStarIsType "migration" (#146); Recommendation: accept
by Ben Gamari 10 Jul '18

10 Jul '18

Hi everyone, We are being asked to consider pull request #146. This proposal is an amendment to the accepted Proposal 0020 [1], removing a migration mechanism which was found in practice to hurt more than help. Specifically, proposal 0020 currently specifies a migration period during which the -XNoStarIsType extension (which proposal 0020 introduces) will be implied by -XTypeOperators. The motivation for this was to ease the transition for packages which use * as a binary type operator. In practice it turned out that a significant number of packages are broken by this migration mechanism. Specifically, many packages use * in kind signatures while also enabling TypeOperators. The proposed amendment removes TypeOperator's implication of NoStarIsType. To be clear, this is ultimately a trade-off between optimising for users of (*) as a binary operator and users of * ~ Type. It just so happens that there are far more of the latter. Consequently, my recommendation is to accept the modified proposal. Cheers, - Ben [1] https://github.com/ghc-proposals/ghc-proposals/pull/83

5 7

Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}
by Simon Peyton Jones 02 Jul '18

02 Jul '18

[Redirecting to the steering committee] I argue for acceptance. * For me a compelling motivation is this: at the moment we can infer types and kinds that we cannot write down with an explicitly-quantified type signature. That seems all wrong to me: we should be able to write down any type you can infer. * The proposal adds notation. It does not add semantics. We already have the distinction between “inferred” and “specified” type variables. You might not like it, but it’s there in GHC. * If it wasn’t there already, I’d be happy to debate not adding it. * If you want to argue for removing the distinction, that would certainly render the current proposal moot. But that would take a GHC proposal – and there are good reasons for the status quo! * What is bad is to maintain the semantic distinction, but be unable to express it. That’s what we have right now, and it’s a bad thing. What is the distinction between “specified” and “inferred”? * Specified. f :: forall a. blah, or f :: a -> a. You may give a visible type argument at a call of f, but you do not have to. Thus (f x) or (f @type x). * Inferred. f :: t a -> t a. The type of f is really g :: forall {k} (t :: k -> *) (a :: k). t a -> t a Note that k does not appear at all in the signature; that’s why it is “inferred”. In GHC today you cannot supply an explicit kind argument for g, but you can supply explicit argument for t and a. So by all means make the case for abolishing the distinction, to render the present proposal moot. But I think it’s unreasonably simply to reject on the grounds of “please think of something better”. Simon From: ghc-devs <ghc-devs-bounces(a)haskell.org> On Behalf Of Iavor Diatchki Sent: 30 April 2018 17:12 To: ghc-devs(a)haskell.org Subject: Discussion on proposal #99: forall {k} Hello, As a shepherd for proposal #99, I'd like to kick off the discussion. The full proposal is available here: https://github.com/goldfirere/ghc-proposals/blob/explicit-specificity/propo… Summary: allows programmers to write `forall {x}` instead of `forall x` in type signatures. The meaning of the braces is that this parameter cannot be instantiated with an explicit type application and will always be inferred. The motivation is to shorten explicit type applications by skipping parameters that are known to be inferable, the common example being omitting the kinds in signatures with poly kinds. As I understand it, the main motivation for this proposals is to give programmers more flexibility when instantiating type variables, with a less noisy syntax. While the proposed solution might work in some situations, I am unconvinced that it is the best way to address the issue in general, for the following reasons: 1. It requires that programmers commit at declaration time about which arguments will be inferred, and which may be inferred or specified. While in some cases this may be an easy decision to make, in many cases this really is a decision which should be made at the use site of a function (e.g., I'd like to provide argument X, but would like GHC to infer argument Y). 2. It still requires that programmers instantiate arguments in a fixed order, which is sometimes dictated by the structure of the type itslef. Here is, for example, what the proposal suggests to do if you want to provide type before a kind: typeRep4 :: forall {k} (a :: k) k'. (k ~ k', Typeable a) => TypeRep a While technically this is not wrong, it is not exactly elegant. I think that we should reject this proposal, and try to come up with a more comprehensive solution to the problem. One alternative design is to allow programmers to instantiate type variables by name. This is much more flexible as it allows programmers to instantiate whichever variables they want, and in whatever order. We've been doing this in Cryptol for a long time, and it seems to work really well. -Iavor

4 22

Or patterns #43 (Round 2.5)
by Manuel M T Chakravarty 29 Jun '18

29 Jun '18

As a reaction to SimonPJ’s suggestion in the ”Round 2” thread https://mail.haskell.org/pipermail/ghc-steering-committee/2018-June/000601.… we have now got a revised revised-proposal for or-patterns at (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 Except for Simon’s reservations, I previously proposed to accept the proposal. Simon wrote that we ought to accept it after the requested change, which has now happened. Hence, I will mark the proposal as accepted *unless* I hear a dissenting opinion by the end of next week. Cheers, Manuel

1 0

Status
by Joachim Breitner 24 Jun '18

24 Jun '18

Hi committee, high time for another status mail. Please look through this and see if anything is pending on you, of otherwise needs your attention. Since the last status update, we * were asked to review these proposals: #112 UnliftedArray# (Shepherd: Simon Marlow) #81 ExtraCommas (Shepherd: Chris) #121 Array resizing primitives (Shepherd: Simon Marlow) #129 TypeApplication and literals (Shepherd: Joachim) #125 Type annotated quoters (Shepherd: Manuel) #111 Linear types (Shepherd: Richard) #28 bundling patterns with type synonyms (Shepherd: Chris) #134 Deprecating Exports (Shepherd: Joachim) #146 Remove TypeOperators => NoStarIsType (Shepherd: Ben) * got a recommendation from shepherds about: #81 ExtraCommas (recommendation: accept) #99 forall {k} (recommendation: accept) #129 TypeApplication and literals (recommendation: accept) #112 UnliftedArray# (recommendation: accept) #121 Array resizing primitives (recommendation: accept) #134 Deprecating Exports (recommendation: accept) #43 Or patterns round two (recommendation: accept) #28 bundling patterns with type synonyms (recommendation: accept) * decided about the following proposals - Constraint vs. Type (accept) - Embrace Type in Type (accept) - PatternSignatures (reject) - Mutable constructor fields (needs revision) #112 UnliftedArray# (accept) #129 TypeApplication and literals (reject) #120 Deriving Via (accept) #103 Treat kind and type vars dientical (accept) #121 Array resizing primitives (accept) #96 Binding existential type variables (reject) We currently have to act on the following 13 proposals, which is one less than last round. Remove TypeOperators => NoStarIsType "migration" https://github.com/ghc-proposals/ghc-proposals/pull/146 Shepherd: Ben Status: Waiting for recommendation. Deprecating Exports https://github.com/ghc-proposals/ghc-proposals/pull/134 Shepherd: Joachim Recommendation: accept Status: Discussion ongoing Type annotated quoters https://github.com/ghc-proposals/ghc-proposals/pull/125 Shepherd: Manuel Status: Waiting for recommendation. Provenance-Qualified Package Imports https://github.com/ghc-proposals/ghc-proposals/pull/115 Shepherd: Ben Status: Waiting for recommendation. Linear types https://github.com/ghc-proposals/ghc-proposals/pull/111 Shepherd: Richard Status: Waiting for recommendation. Define Kinds Without Promotion https://github.com/ghc-proposals/ghc-proposals/pull/106 Shepherd: Ryan Status: Still waiting for recommendation. forall {k}, https://github.com/ghc-proposals/ghc-proposals/pull/99 Shepherd: Iavor Status: Ongoing discussion ExtraCommas https://github.com/ghc-proposals/ghc-proposals/pull/87 Shepherd: Chris Recommendation: accept Status: Ongoing discussion, met with some reservation. Visible dependent quantification (TL;DR: forall k -> k -> *) https://github.com/ghc-proposals/ghc-proposals/pull/81 Shepherd: Roman Leshchinskiy Status: Discussion needs to happen Top-level kinds signatures https://github.com/ghc-proposals/ghc-proposals/pull/54 Shepherd: Roman Leshchinskiy Status: Waiting for recommendation. Or-Patterns https://github.com/ghc-proposals/ghc-proposals/pull/43 Shepherd: Manuel Recommendation: accept Status: Round 2 being discussed Lazy unboxed tuples https://github.com/ghc-proposals/ghc-proposals/pull/35 Shepherd: Ryan Status: This is still lingering since last July! Bundling patterns with synonyms https://github.com/ghc-proposals/ghc-proposals/pull/28 Shepherd: Chris Recommendation: accept Status: Ongoing discussion, met with some resistance. Cheers, Joachim -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

1 0

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

Please Review: Remove TypeOperators => NoStarIsType "migration" (#146), Shepherd: Ben Gamari
by Joachim Breitner 23 Jun '18

23 Jun '18

Dear Committee, this is your secretary speaking: Remove TypeOperators => NoStarIsType "migration" #146 by Oleg Grenrus was proposed. https://github.com/ghc-proposals/ghc-proposals/pull/28 I propose Ben Gamari as the shepherd, in case the decision needs to be coordinated with the 8.6 release. Ben, 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 -- Joachim Breitner mail(a)joachim-breitner.de http://www.joachim-breitner.de/

2 1