Re: Partial type synonyms -- first-class!

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 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 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ő 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/e8be2cb2b1093275385467741b129... )

* Changing `isCompleteHsSig` to run in `TcM`, so that its result can depend on type constructor details ( https://gitlab.haskell.org/cactus/ghc/-/commit/49f60ef13ad7f63f91519ca88cd80... )

* 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