<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jul 22, 2022, at 4:53 AM, Simon Peyton Jones <<a href="mailto:simon.peytonjones@gmail.com" class="">simon.peytonjones@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: tahoma, sans-serif; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">expand them during</span><br style="caret-color: rgb(0, 0, 0); font-family: tahoma, sans-serif; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><span style="caret-color: rgb(0, 0, 0); font-family: tahoma, sans-serif; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: 400; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">typechecking,</span></div></blockquote></div><br class=""><div class="">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.)</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">type T a = forall b. b -> Either a b</div><div class=""><br class=""></div><div class="">meaning to take the `forall b` and lift it to the top of whatever type T appears in. So that</div><div class=""><br class=""></div><div class="">f :: [a] -> T a</div><div class=""><br class=""></div><div class="">would really mean</div><div class=""><br class=""></div><div class="">f :: forall a b. [a] -> b -> Either a b</div><div class=""><br class=""></div><div class="">and not</div><div class=""><br class=""></div><div class="">f :: forall a. [a] -> forall b. b -> Either a b</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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</div><div class=""><br class=""></div><div class="">type T a = b -> Either a b</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Good luck with the implementation, Gergo!</div><div class="">Richard</div></body></html>