Partial type synonyms -- first-class!

Thu Aug 11 17:37:50 UTC 2022

> On Aug 5, 2022, at 6:17 AM, ÉRDI Gergő <gergo at erdi.hu> wrote:
> 
> 1. Defining partial type synonyms
> 

This makes some sense to me. You're introducing a new form of invisible (implicit) parameter, adding to the two we already have. Today, we have

A. invisible parameters that are filled in via unification. We write these in types as `forall a.`
B. invisible parameters that are filled in via looking for a unique inhabitant of a type. We write these in types as `C a =>`

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.

> 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.

> 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.

> 
> 1. How do I find the wildcard-originating tyvars robustly? Currently,
> I am using `candidateQTyVarsWithBinders` but that picks up "regular"
> out-of-scope tyvars as well. I believe this causes a regression of
> #17567; furthermore, it means if the user writes `type Syn a = Foo b` it
> is handled the same as if they wrote `type Syn a = Foo _`, but it would
> be better to reject it instead.

Yes, sadly I think that you may have to add a new bit of information to e.g. TauTv to do this. Sad, but I can't think of another way.

> 
> 2. What should the `Role` of these implicit type parameters be? For
> now, I've went with `Nominal` for lack of a better answer.

Answered by you.

> 
> 3. When typechecking a type application, I need to insert wildcards
> for these implicit arguments. I am currently using `AnonTCB InvisArg`
> binders to represent these implicit type parameters, which means by
> the time I get to `tcInferTyApps`, they would get passed through
> `instantiate` to `tcInstInvisibleTyBinder`. I currently have a
> horrible kuldge here to check, before calling
> `tcInstInivisibleTyBinder`, that the invisible binder's kind doesn't
> meet the preconditions of it; and if it doesn't, I create a wildcard
> instead. But of course, it would be nicer if I could put something in
> the `TcTyConBinder` that identifies these binders properly.

Yes, I think AnonTCB InvisArg will get you into trouble, because that's what's used for class constraints. As I observed earlier, you're creating a new form of quantification, and so InvisArg doesn't quite say what you want. Make a new constructor.

> On Aug 8, 2022, at 10:08 PM, Gergő Érdi <gergo at erdi.hu> wrote:
> 
> 2. It turns out I misunderstood the `Role` situation and they are
> actually computed via some weird knot tying from the `TyCon` itself.
> So on one hand, I don't really need to do anything to "come up with"
> roles for these implicit type parameters. On the other hand, I think
> this also means that this breaks the surface syntax for role
> declarations, since the user would be expected to give roles for type
> parameters they never explicitly added to their tysyns...

Type synonyms do not support role annotations, so we can dodge this bullet. Just let the weird knot tying thing do its work and stay out of the way. :)

> 
> 3. Similar to #1, I started just pushing all the way through GHC a
> change to `AnonArgFlag` that adds a third `ImplArg` flag. It is
> handled mostly the same way as an `InvisArg`, except `tcInferTyApps`
> can use it to insert wildcard arguments. I don't have a full commit
> for this yet.

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.

> 
> Beside comments on this approach, I would also like to hear from Simon
> & Richard if they agree that with this new approach, this could now be
> a real language feature that could get upstreamed once all these
> implementation wrinkles are smoothed out.

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.

Given your design, however, I think the implementation you describe is reasonable. I have not read the code you linked to.

I hope this helps!

Richard

> Thanks,
>  Gergo
> 
> On Fri, Aug 5, 2022 at 6:17 PM ÉRDI Gergő <gergo at erdi.hu> wrote:
>> 
>> As I mentioned at the end of the original thread (but probably no one
>> was interested in this enough to read that far), after a breakthrough
>> idea I have now started working on partial type synonyms that are NOT
>> just defined using macro expansion semantics, and indeed can be a
>> first-class abstraction. I think if I can iron out the wrinkles
>> detailed at the bottom of this message, this would be good for a GHC
>> proposal.
>> 
>> 1. Defining partial type synonyms
>> 
>> The idea is to typecheck the type synonym declaration
>> 
>>     type Syn a = MyType _ [a] Int
>> 
>> into a type synonym that has some implicit (invisible) type parameters:
>> 
>>     type Syn {w1} a = MyType w1 [a] Int
>> 
>> We don't need to come up with any new design for "what this means":
>> this means exactly the same as
>> 
>>     type Syn w1 a = MyType w1 [a] Int
>> 
>> which is something you can already write today. The only difference is
>> how `w1` is given at use sites.
>> 
>> 2. Using partial type synonyms
>> 
>> When a partial type synonym is applied, its argument list is expanded
>> by adding wildcard arguments for the invisible parameters. So this use
>> site:
>> 
>>     Syn Double
>> 
>> is typececked into the type application
>> 
>>     Syn {_} Double
>> 
>> Again, we don't need to come up with any new design for "what this
>> means": this is the same as writing `Syn _ Double` into the same
>> position, it's just the `_` is not written in the surface syntax.
>> 
>> In particular:
>> 
>>   * The level of the type variable conjured for the `_` is determined
>>     fully by where the `Syn Double` occurs, and not at all by the
>>     definition of `Syn`
>> 
>>   * Using the type synonym `Syn` is only valid where a wildcard
>>     occurrence would be valid. In particular, using `Syn` in a type
>>     signature causes the signature itself to be regarded as partial
>>     (`isCompleteHsSig` returns `False` for it).
>> 
>> 3. Implementation
>> 
>> I have a proof-of-concept implementation at
>> https://gitlab.haskell.org/cactus/ghc/-/compare/master...cactus%2Fpartial-tysyns?from_project_id=1117
>> 
>> I tried to make it as small a change as I could. Its key points are:
>> 
>>   * In the renamer, we allow wildcards in `TySynCtx` context
>> 
>>   * In `tcTySynRhs`, we allow wildcards in the right-hand side,
>>     retrieve them from the result of typechecking, and intersperse
>>     them with the "normal" type parameters to get a well-scoped
>>     telescope.
>> 
>>   * About a third of the lines changed is just a boring refactoring of
>>     `isCompleteHsSig` to be able to look up type synonym
>>     `TyCon`s. This is needed because a type signature referring to
>>     partial type synonyms will be partial itself once those type
>>     synonym applications are elaborated.
>> 
>>   * When typechecking a type application, implicit arguments get
>>     filled with the result of `tcAnonWildCardOcc`.
>> 
>> Now, my questions about the problems I've encountered along the way. I
>> hope these questions are concrete enough that I can get concrete
>> answers to them from this list:
>> 
>> 1. How do I find the wildcard-originating tyvars robustly? Currently,
>> I am using `candidateQTyVarsWithBinders` but that picks up "regular"
>> out-of-scope tyvars as well. I believe this causes a regression of
>> #17567; furthermore, it means if the user writes `type Syn a = Foo b` it
>> is handled the same as if they wrote `type Syn a = Foo _`, but it would
>> be better to reject it instead.
>> 
>> 2. What should the `Role` of these implicit type parameters be? For
>> now, I've went with `Nominal` for lack of a better answer.
>> 
>> 3. When typechecking a type application, I need to insert wildcards
>> for these implicit arguments. I am currently using `AnonTCB InvisArg`
>> binders to represent these implicit type parameters, which means by
>> the time I get to `tcInferTyApps`, they would get passed through
>> `instantiate` to `tcInstInvisibleTyBinder`. I currently have a
>> horrible kuldge here to check, before calling
>> `tcInstInivisibleTyBinder`, that the invisible binder's kind doesn't
>> meet the preconditions of it; and if it doesn't, I create a wildcard
>> instead. But of course, it would be nicer if I could put something in
>> the `TcTyConBinder` that identifies these binders properly.
>> 
>> Thanks in advance,
>>        Gergo
>> 
>> --
>> 
>>   .--= ULLA! =-----------------.
>>    \     http://gergo.erdi.hu   \
>>     `---= gergo at erdi.hu =-------'
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs