Partial type synonyms -- first-class!

Fri Aug 12 03:05:05 UTC 2022

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 <ekmett at 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ő <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
>>
> _______________________________________________
> 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/20220812/709754e5/attachment.html>