Partial type synonyms -- first-class!

Wed Aug 17 21:53:46 UTC 2022

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 <gergo at 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 <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
>>
> _______________________________________________
> 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/20220817/22c98db1/attachment.html>