> On Jul 22, 2022, at 4:53 AM, Simon Peyton Jones <simon.peytonjo...@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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
