Wildcards in type synonyms

[Richard Eisenberg]

> On Jul 22, 2022, at 4:53 AM, Simon Peyton Jones <simon.peytonjones at gmail.com> wrote:
> 
> expand them during
> typechecking,

Just to expand on this point (haha): your new type macros (distinct from type synonyms) would have to be eagerly expanded during type checking. You say this (quoted above), but I wanted to highlight that this is in opposition to the way today's type synonyms work, which are expanded only when necessary. (Rationale: programmers probably want to retain the very clever synonym name they came up with, which is hopefully easier to reason about.)

Interestingly, type macros may solve another problem that has come up recently: Gershom proposed (a quick search couldn't find where this was, but it was around restoring deep-subsumption behavior) a change to the way polytypes work in type synonyms. Specifically, he wondered about, e.g.

type T a = forall b. b -> Either a b

meaning to take the `forall b` and lift it to the top of whatever type T appears in. So that

f :: [a] -> T a

would really mean

f :: forall a b. [a] -> b -> Either a b

and not

f :: forall a. [a] -> forall b. b -> Either a b

as it does today. With deep subsumption, you can spot the difference between these types only with type applications, but they are incomparable types with simple subsumption.

At the time, I didn't understand what the semantics of Gershon's new type synonyms were, but in the context of Gergo's type macros, they make sense. To wit, we could imagine

type T a = b -> Either a b

Note: b is unbound. This is actually a type *macro*, not a type synonym, and it expands to a form that mentions a free variable b. (Presumably, this b would not capture a b in scope at the usage site.) This macro behavior delivers what Gershom was looking for.

I'm not saying Gergo should necessarily implement this new aspect of type macros (that don't mention wildcards), but if this ever does come to a proposal, I think these kind of variables are a new motivator for such a proposal. I'd probably favor some explicit notation to introduce a macro (e.g. `type macro T a = Either _ a`) instead of using a syntactic marker like the presence of a _ or an unbound variable, but we can debate that later.

Good luck with the implementation, Gergo!
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220722/49fb1f73/attachment.html>