May 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

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

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

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

Need more Trac tickets
by Richard Eisenberg 03 Jun '18

03 Jun '18

Hi all, Ryan Scott very helpfully this morning labeled the Trac tickets that have grown from proposals. However, there remain a good many proposals without corresponding Trac tickets. I propose that we make it a shepherd's responsibility to make sure that a Trac ticket is created upon the acceptance of a proposal. Specifically: a shepherd should encourage the proposer to make the Trac ticket, and if this fails to happen, then for the shepherd to do it himself. (Why have the proposer do it? 1. To lessen the burden on the shepherd. 2. To subtly encourage the proposer to ponder the possibility of implementing.) What do we think? We'll still have to make tickets for those accepted proposals but with not tickets... Richard

2 5

Array resizing primitives (#121), proposal: accept with modifications
by Simon Marlow 03 Jun '18

03 Jun '18

I propose that we accept https://github.com/ghc- proposals/ghc-proposals/pull/121 With one modification (below). In summary, this proposal suggests adding primitives for resizing (shrinking or expanding) primitives mutable arrays of pointers. See the proposal for motivation. There would be two primitives per array type: shrinkArray# :: MutableArray# s a -> Int# -> State# s -> State# s resizeArray# :: MutableArray# s a -> Int# -> a -> State# s -> (# State# s, MutableArray# s a #) (these mirror the existing shrink and resize primitives we have for ByteArray#, with the same rationale) The biggest downside is that we currently have sizeOfMutableArray# :: MutableArray# s a -> Int # which would need to be replaced by a stateful operation getSizeOfMutableArray# :: MutableArray# s a -> State# s -> (# State# s, Int# #) So we would need to deprecate the old primops, update any code we have that uses them, and clearly indicate the unsafety in the docs. But this has knock-on effects in Data.Primitive: sizeofMutableArray :: MutableArray s a -> Int this would need to be deprecated and replaced by a PrimMonad operation. The pure version would be unsafe in the sense that it could return the wrong size, and a future indexing operation relying on the incorrect size could access an out-of-bounds element. Suggested modifications: * Remove the ArrayArray# primitives, add UniftedArray# primitives instead (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0021-u… ) Cheers Simon On 1 May 2018 at 13:12, Joachim Breitner <mail(a)joachim-breitner.de> wrote: > Dear Committee, > > this is your secretary speaking: > > Array resizing primitives have been proposed by David Feuer: > https://github.com/ghc-proposals/ghc-proposals/pull/121 > > I propose Simon Marlow as the shepherd. > > Simon, 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/ > > _______________________________________________ > ghc-steering-committee mailing list > ghc-steering-committee(a)haskell.org > https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee > >

3 2

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