Partial type synonyms -- first-class!

Fri Aug 12 02:42:56 UTC 2022

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ő <gergo at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220811/702c4974/attachment.html>