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 <[email protected]> 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ő <[email protected]> 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 >> [email protected] >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > _______________________________________________ > ghc-devs mailing list > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
