Richard writes I think the route you're taking is a reasonable route to your destination, > but I'm not yet convinced it's a destination I want GHC to travel to. >
I'm in the same boat -- not yet convinced. To me it seems like quite a bit of implementation complexity to hit a pretty narrow use-case. But maybe you have convincing use-cases to offer, when you write a proposal. (Maybe Edward can help with some.) In any case, it's not me or Richard you need to convince, it's the GHC Steering Committee via the proposals process. You are doing a great job of working out an implementation before submitting a proposal (which few people do), but that doesn't, in and of itself, make the design more attractive. Yet it must be very attractive to you if you are contemplating maintaining a fork in the medium term. Maybe you can convince everyone! Simon On Fri, 12 Aug 2022 at 04:05, Gergő Érdi <ge...@erdi.hu> wrote: > That's great to hear because it looks like this will need all the support > it can get to ever be allowed into upstream... > > On Fri, Aug 12, 2022, 10:43 Edward Kmett <ekm...@gmail.com> wrote: > >> FWIW, Gergo, I've been following what you've been doing pretty closely, >> so there's at least two of us tracking it in the background. =) I might >> have some clever(?) (ab)uses for it in the future in my linear haskell code. >> >> -Edward >> >> On Thu, Aug 11, 2022 at 10:33 PM ÉRDI Gergő <ge...@erdi.hu> wrote: >> >>> Hi Richard, >>> >>> Thanks for getting back to me! My replies are inline below. >>> >>> On Thu, 11 Aug 2022, Richard Eisenberg wrote: >>> >>> > You want a third: >>> > >>> > C. invisible parameters that are filled in with a fresh wildcard. >>> > >>> > We would need to have some way of writing out the type of such a thing >>> > (i.e. what kind would `Syn` have?), but I presume this is possible. >>> >>> I think there's a tension between this and your suggestion to only add >>> implicit parameters as a new `TyConBndrVis`, but more on that below. >>> >>> >> 2. Using partial type synonyms >>> >> >>> >> >>> > >>> > This bit also makes sense, but I think users will want more >>> > functionality. Specifically, what if a user does not want a wildcard >>> > inserted, because they know that the right choice is `Int`? Or maybe >>> > they want a *named* wildcard inserted. My experience is that once >>> > something can be done implicitly, folks will soon find good reasons to >>> > do it explicitly on occasion. >>> >>> Good point, but I think we can punt on this and not close any doors >>> ahead. >>> So today, you would only be able to write `Syn T` to mean `Syn {_} T`, >>> and >>> then in the future we can add typechecker support (and new surface >>> syntax!) for `Syn {S} T`, without causing any compatibility problems >>> with >>> any existing code that doesn't give explicit args for implicit params. >>> >>> >> 3. Implementation >>> >> >>> >> >>> >> * When typechecking a type application, implicit arguments get >>> >> filled with the result of `tcAnonWildCardOcc`. >>> > >>> > What about named wildcards? Even if they're not passed in, perhaps >>> someone wants >>> > >>> > type SomeEndo = _t -> _t >>> > >>> > where the two types are known to be the same, but we don't know what. >>> >>> This would be something to support when typechecking the definition, not >>> a >>> given application. Your example would still elaborate to >>> >>> type SomeEndo {t} = t -> t >>> >>> it would just use the same implicitly-bound type parameter `t` twice on >>> the right-hand side. But when you use `SomeEndo`, the usage would still >>> elaborate into a (single) anonymous wildcard argument, i.e. >>> `SomeEndo {_}`. >>> >>> My current implementation doesn't support your example, but I think it's >>> only because the renamer rejects it. I think if I get it through the >>> renamer, it should already work because that `_t` will typecheck into a >>> wildcard `TauTv`. >>> >>> >> 3. Similar to #1, I started just pushing all the way through GHC a >>> >> change to `AnonArgFlag` that adds a third `ImplArg` flag. >>> > >>> > I don't love adding a new constructor to AnonArgFlag, because that's >>> > used in terms. Instead, it would be great to localize this new >>> extension >>> > to tycon binders somehow. >>> >>> OK so while I'd love to get away with only changing `TyConBndrVis`, this >>> is the part of your email that I don't understand how to do :/ >>> >>> First, when a type application is typechecked, we only have the kind of >>> the type constructor, not its binders (and that makes sense, since we >>> could be applying something more complex than directly a defined type >>> constructor). So if I only add a new `TyConBndrVis` constructor, then I >>> have no way of representing this in the `tyConKind` and so no way of >>> finding out that I need to put in implicit args in `tcInferTyApps`. >>> >>> Second, you ask what the kind of `Syn` in e.g. `type Syn a = TC _ a` is. >>> I >>> think (supposing `TC :: K -> L -> M`) its kind should be (stealing >>> syntax >>> from Agda) something like `{K} -> L -> M`, i.e. a function kind with >>> domain `K`, codomain `L -> M`, and a new kind of visibility on the arrow >>> itself. But that means it's not just the binder of the implicit >>> parameter >>> that has a new visibility, but the arrow as well. And isn't that what >>> `AnonArgFlag` is for? >>> >>> > I think the route you're taking is a reasonable route to your >>> > destination, but I'm not yet convinced it's a destination I want GHC >>> to >>> > travel to. As I hint above, I think the feature would have to be >>> > expanded somewhat to cover its likely use cases, and yet I worry that >>> it >>> > will not be widely enough used to make its specification and >>> > implementation worthwhile. I'm happy to be convinced otherwise, though. >>> >>> Fair enough. Although I was hoping that with Dependent Haskell, we would >>> have more situations where unification can give useful solutions, and so >>> we would want the feature of implicit arguments (even for terms!). >>> >>> But if there's no appetite from GHC for partial type synonyms, what >>> would >>> help me a lot in keeping this maintainable / avoiding churn in chasing >>> `master` would be if I can upstream two refactorings that are enablers >>> for my implementation but don't actually change any existing behaviour: >>> >>> * Adding "does it come from a wildcard" flag to `TauTv` >>> ( >>> https://gitlab.haskell.org/cactus/ghc/-/commit/e8be2cb2b1093275385467741b1297ce91ef7547 >>> ) >>> >>> * Changing `isCompleteHsSig` to run in `TcM`, so that its result can >>> depend on type constructor details >>> ( >>> https://gitlab.haskell.org/cactus/ghc/-/commit/49f60ef13ad7f63f91519ca88cd8095db0781c92 >>> ) >>> >>> * Maybe a third one, depending on what we come up with for the >>> representation of these implicit binders >>> >>> What do you think about this? >>> >>> Thanks, >>> Gergo >>> _______________________________________________ >>> ghc-devs mailing list >>> ghc-devs@haskell.org >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >>> >> _______________________________________________ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > _______________________________________________ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs