- ghc-steering-committee

Re: [ghc-steering-committee] Discussion on proposal #99: forall {k}
by Richard Eisenberg 03 Jul '18

03 Jul '18

Yes -- it's a property of the type. This aspect wasn't highlighted in the original proposal because it's not a change. Types *already* have this inferred/specified distinction (and have since GHC 8.0), but users can't directly access the feature. This proposal is all about -- and only about -- concrete syntax. Richard

2 1

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

02 Jul '18

It’s already present in the implementation, but it’s not already present in any explicitly-stated language proposal. So this proposal might be a good opportunity to fix that deficiency. S From: Richard Eisenberg <rae(a)cs.brynmawr.edu> Sent: 02 July 2018 13:23 To: Simon Peyton Jones <simonpj(a)microsoft.com> Cc: Iavor Diatchki <iavor.diatchki(a)gmail.com>; ghc-steering-committee(a)haskell.org; Joachim Breitner <mail(a)joachim-breitner.de> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} Yes -- it's a property of the type. This aspect wasn't highlighted in the original proposal because it's not a change. Types *already* have this inferred/specified distinction (and have since GHC 8.0), but users can't directly access the feature. This proposal is all about -- and only about -- concrete syntax. Richard On Jul 2, 2018, at 4:49 AM, Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: It really is not quite clear if the specificity is a property of the type itself, or the thing that has that type. I think Richard has clarified now, right? It’s a property of a type. Simon From: Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> Sent: 29 June 2018 19:26 To: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> Cc: Richard Eisenberg <rae(a)cs.brynmawr.edu<mailto:rae@cs.brynmawr.edu>>; ghc-steering-committee(a)haskell.org<mailto:ghc-steering-committee@haskell.org>; Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} I am supportive of accepting the proposal, but I think that we should address the point raised by Joachim on the the git-hub thread first (https://github.com/ghc-proposals/ghc-proposals/pull/99#issuecomment-4010609…<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com…>). It really is not quite clear if the specificity is a property of the type itself, or the thing that has that type. On Thu, Jun 28, 2018 at 1:07 AM Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: I’m keen on this proposal. I am very keen to be able to express in a type or kind signature everything needful to use the value (or type constructor). The proposal gives an example at the term level. It’d be strengthened by an example at the type level. Eg type T1 :: forall {k}. (k->Type) -> k -> Type data T1 f a = MkT (f a) type T2 :: forall k. (k->Type) -> k -> Type data T2 f (a::k) = MkT2 (f a) Here T1 has an inferred kind variable, mentioned nowhere in the declaration. The kind signature (which I have written as if it were code, which is the subject of a separate proposal) is inferred as shown. T2 mentions k, so its kind signature looks a bit different. What’s the difference? It’s exactly in explicit kind application. You can write (T1 @Type Maybe Int), but T2 can’t have that explicit kind argument. The whole business of Required/Specified/Inferred is more complicated than I like, but if we have it (which we do right now) we should allow the programmer to specify exactly what they mean. (An alternative is to abolish the Specified/Inferred distinction, but that carries significant costs of its own and no one is proposing it.) Let’s accept! Simon From: Richard Eisenberg <rae(a)cs.brynmawr.edu<mailto:rae@cs.brynmawr.edu>> Sent: 28 June 2018 05:45 To: Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> Cc: Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>>; ghc-steering-committee(a)haskell.org<mailto:ghc-steering-committee@haskell.org>; Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} But we morally *do* have explicit kind application. See accepted proposal https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0015-t…<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com…> So the only reason that we don't have it is that GHC hasn't caught up to its specification. (I have a student working on this now.) The reason that T2 and T3 are different here is that T2 mentions the k in the type declaration, while T3 mentions it only in the constructor declaration. Richard On Jun 26, 2018, at 6:52 PM, Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> wrote: Hello, thanks for the revisions---I read through the new version, and I think I almost understand the plan. I would say that for this proposal it makes more sense to just deal with explicit specificities at the value level, and never have the curly braces in type constructors. Since we don't have an explicit kind application at the type level (e.g., we can't write `Proxy @Type`), I don't think it really makes sense to add the braces to type constructors. If we ever implemented THAT feature, then we can discuss which declarations should have explicit and which should have implicit parameters. In the current set of examples, I find it odd that `T2` does not have braces, but `T3` does. -Iavor On Wed, Jun 20, 2018 at 2:15 PM Richard Eisenberg <rae(a)cs.brynmawr.edu<mailto:rae@cs.brynmawr.edu>> wrote: I have posted the new proposal, at https://github.com/ghc-proposals/ghc-proposals/pull/148<https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com…> I've also updated #99 to clarify where the new syntax is allowed. For Iavor's examples: data T1 a = C1 a type T1 :: Type -> Type C1 :: forall a. a -> T1 a data T2 (a :: k) = C2 { f2 :: Proxy a } type T2 :: forall k. k -> Type C2 :: forall k (a :: k). Proxy a -> T2 a f2 :: forall k (a :: k). T2 a -> Proxy a data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a type T3 :: forall {k}. k -> Type C3 :: forall k (a :: k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a type T4 :: forall {k}. k -> Type C4 :: forall {k} (a :: k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a Rejected, as k is used dependently but is not lexically dependent. (This is no change.) It we have > data T5 k (a :: k) where C5 :: forall k (a :: k). Proxy a -> T5 k a we would get type T5 :: forall k -> k -> Type C5 :: forall k (a :: k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a Rejected, like T6. If we revise to: > data T6 k (a :: k) where C6 :: forall {k} (a::k). Proxy a -> T6 k a we get type T6 :: forall k -> k -> Type C6 :: forall {k} (a::k). Proxy a -> T6 k a I've updated the proposal itself to include these examples. Does this help to clarify? Richard On May 25, 2018, at 1:56 PM, Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> wrote: Hello, well, I thought that Richard was going to write a new proposal based on the feedback here, but it sounds like he is planning to revise #99, and then write a separate new one. I guess we should discuss the proposal again once the changes are in. I would encourage Richard to add some text and examples to clarify exactly what's in the proposal and what's not, and how things are supposed to work. Here are some examples, for which it would be illuminating (to me) to see the types/kinds of all names introduced. data T1 a = C1 a data T2 (a :: k) = C2 { f2 :: Proxy a } data T3 a where C3 :: forall k (a::k). Proxy a -> T3 a data T4 a where C4 :: forall {k} (a::k). Proxy a -> T3 a data T5 k a where C5 :: forall k (a::k). Proxy a -> T5 k a data T6 k a where C6 :: forall {k} (a::k). Proxy a -> T6 k a -Iavor On Fri, May 25, 2018 at 2:02 AM Simon Peyton Jones <simonpj(a)microsoft.com<mailto:simonpj@microsoft.com>> wrote: I’m keen to get #99 into GHC in some form. My motivation (which could be a fourth bullet in the proposal) is that it should be possible for a programmer to write a fully-explicit type signature for anything GHC can infer. But currently we can’t. For typeRep1 GHC infers the signature shown for typeRep3; but we can’t write it down. based on the discussion so far, it seems that #99 in its current form might not be exactly what we want Can you summarise the reasons it might not be exactly what we want? Simon From: ghc-steering-committee <ghc-steering-committee-bounces(a)haskell.org<mailto:ghc-steering-committee-bounces@haskell.org>> On Behalf Of Richard Eisenberg Sent: 24 May 2018 21:17 To: Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> Cc: ghc-steering-committee(a)haskell.org<mailto:ghc-steering-committee@haskell.org>; Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> Subject: Re: [ghc-steering-committee] Discussion on proposal #99: forall {k} I do plan on turning Joachim's recent suggestion into a separate proposal, and then to modify #99. But the modification would remove only the bit about classes, not the feature overall. I don't have time to do this now, though -- will do next week. Richard On May 24, 2018, at 1:54 PM, Iavor Diatchki <iavor.diatchki(a)gmail.com<mailto:iavor.diatchki@gmail.com>> wrote: Hello, based on the discussion so far, it seems that #99 in its current form might not be exactly what we want, so I'd say that we should reject it for the moment. Overall, I agree that it would be nice to come up with a consistent notation for things that are currently happening in GHC but we can't write, so perhaps we could revisit this with a revised proposal at a later time? -Iavor On Sat, May 5, 2018 at 8:48 PM Joachim Breitner <mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de>> wrote: Hi, Am Mittwoch, den 02.05.2018, 16:10 -0400 schrieb Richard Eisenberg: > Joachim, you are always a fount of interesting ideas. > > > On May 2, 2018, at 2:51 PM, Joachim Breitner <mail@joachim-breitner > > .de> wrote: > > > > class C k (a : k) where meth :: a > > meth :: forall {k} a. C k a -> k -> Constraint > > I think this is brilliant. But not only for this proposal! Imagine > this: > > class Num a where > fromInteger :: Integer -> a > > fromInteger :: Integer -> forall a. Num a => a > > If we do that, then #129 is essentially solved, at no further cost to > anyone. (Note that in all Haskell98-style code, no one will ever be > able to notice the changed type of fromInteger.) > > This approach also allows for the possibility of reordering > quantified type variables for Haskell98-style constructors, if anyone > should want to do it. > > And it allows for updated types (including quantified variable > ordering, etc.) for record selectors. > > And it allows (maybe?) for giving good types to GADT record > selectors: > > data X a where > Foo :: { bar :: Int } -> X Int > Quux :: { bar :: Bool } -> X Bool > bar :: X a -> a > > GHC currently rejects the declaration for X, but it could be accepted > if only we could specify the correct type of bar. And now we can. I > don't particularly want to cook up the typing rules here, but I don't > think I'm totally crazy. > > GADT record selectors aside, the rule for these could be that the > top-level type signature must be equivalent w.r.t. the subtype > relation with the original type signature. That is, if the new > signature is t1 and the old was t2, then t1 <: t2 and t2 <: t1. Easy > enough to check for. The implementation would probably do a little > worker/wrapper stunt. I smell a new proposal… what does this mean for #99? Will you want to revise it? Cheers, Joachim -- Joachim Breitner mail(a)joachim-breitner.de<mailto:mail@joachim-breitner.de> http://www.joachim-breitner.de/<https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fwww.joachim…> _______________________________________________ ghc-steering-committee mailing list ghc-steering-committee(a)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(a)haskell.org<mailto:ghc-steering-committee@haskell.org> https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee

1 0

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

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

19 Jun '18

We now have a revised version of the ”Or pattern” proposal #43 to consider: (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 You may remember that we discuss this a while back https://mail.haskell.org/pipermail/ghc-steering-committee/2017-November/000… and finally decided to bounce it back to the authors with the following recommendation: https://github.com/ghc-proposals/ghc-proposals/pull/43#issuecomment-3581893… We previously decided that we are inclined to accept this proposal if the authors change the points that we highlighted. Judging from the conversation of SimonPJ and Richard with the author on the GitHub thread, it appears to me that most of the issues have been addressed. However, Simon’s point • "Patterns that bind existentials, dictionaries, or equalities are rejected by the type checker". I disagree. Earlier I suggested "no variable bound by an or-pattern can have a type that mentions an existential variable bound by the or-pattern". That is much more friendly because you can still match against an existential constructor; you just can’t bind an existential variable. from <https://github.com/ghc-proposals/ghc-proposals/pull/43#issuecomment-3689334… <https://github.com/ghc-proposals/ghc-proposals/pull/43#issuecomment-3689334…>> still doesn’t seem to be addressed, or am I misunderstanding? Overall, I propose to accept the proposal, possibly requiring that the above point be addressed. What do you all think? Cheers, Manuel

4 5

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

Kinds without promotion (#106)
by Iavor Diatchki 14 Jun '18

14 Jun '18

Hello, it's been a couple of months since this was submitted to the committee, so I'd be interested to get some feedback. In summary, this proposal introduces a mechanism for defining new kinds without having to promote a datatype, thus avoiding pollution of the value level name space with unused constructors. This is not a particularly new idea, and folks have been asking for it for at least 6 years now (e.g., see #6024). A few of our projects at work make use of a lot of type-level indexing (using GATs, etc.) and while things mostly work pretty well, the clunkiness of having to promote datatypes when you just want to define a new kind is something that keeps popping up over and over again, which is why I was motivated to submit the proposal. Thoughts? -Iavor

1 0