Wildcards in type synonyms

[Simon Peyton Jones]

>
> So it seems that instead of shoehorning it into the existing type
> synonyms, a better bet would be to branch off to a separate path quite
> early (maybe as soon as during renaming), expand them during
> typechecking, and *not* touch how/when existing "normal" type synonyms
> are resolved.
>

That sounds plausible, yes.

Simon

On Fri, 22 Jul 2022 at 09:50, Gergő Érdi <gergo at erdi.hu> wrote:

> Thanks Simon, these are very useful hints. My plan is to just push
> ahead on a separate fork, with this "macro semantics", and maybe if it
> comes out nicer than I'd hope, I'll propose it.
>
> So it seems that instead of shoehorning it into the existing type
> synonyms, a better bet would be to branch off to a separate path quite
> early (maybe as soon as during renaming), expand them during
> typechecking, and *not* touch how/when existing "normal" type synonyms
> are resolved.
>
> On Fri, Jul 22, 2022 at 4:14 PM Simon Peyton Jones
> <simon.peytonjones at gmail.com> wrote:
> >
> > Hi Gergo
> >
> >> I'd like to implement type synonyms containing wildcards. The idea is
> >> that if you have `type MySyn a = MyType a _ Int`, then during
> >> typechecking, every occurrence of `MySyn T` would be expanded into
> >> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
> >
> >
> > I imagine you mean that if you then write
> > f :: MySyn a -> a -> Int
> > then it's exactly as if you wrote (using PartialTypeSignatures)
> > f :: MyType a _ Int -> a -> Int
> > today.   So if I understand it right, you intend that these type
> synonyms are second-class citizens: they can occur precisely (and only)
> where wildcards are allowed to occur today.  For example, as Iavor
> suggests, you'd reject
> > data T a = MkT (MySyn a)
> >
> > If you want to do this in a fork of GHC, that's obviously fine. If you
> want to offer it as a language extension, the best thing would be to write
> a GHC Proposal.  Also you'd get a lot of useful design feedback that way,
> which might save you implementation cycles.
> >
> >> What is the reason for this? I would have expected type synonyms to be
> >> only relevant during typechecking, and then fully resolved in the
> >> elaborated Core output.
> >
> >
> > In GHC an Id has only one type.   It does not have a "source type" and a
> "Core type".  So we allow Core types to contain synonyms so that when we
> export that Id the importing scope (e.g. GHCi, and type error messages) can
> see it.  Synonyms can also allow types to take less space. E.g.  we have
> Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep).  One
> could imagine a different design.
> >
> > I would expect that, by the time typechecking is over, all your wildcard
> synonyms are gone.  They really are second class.
> >
> > Just to mention too that the entire "wildcards in type signatures" story
> is (I think) jolly useful, but it also turned out to be pretty tricky to
> implement.  If you just macro-expand your new synonyms, you won't disturb
> the wildcard story, but I just wanted to advertise that it's a tricky area.
> >
> > Simon
> >
> > On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő <gergo at erdi.hu> wrote:
> >>
> >> Hi,
> >>
> >> I'd like to implement type synonyms containing wildcards. The idea is
> >> that if you have `type MySyn a = MyType a _ Int`, then during
> >> typechecking, every occurrence of `MySyn T` would be expanded into
> >> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
> >>
> >> One worrying thing I noticed in my initial exploration of the GHC
> >> codebase is that the Core representation of `Type`s can still contain
> >> type synonym occurrences. And this doesn't seem like just an artefact
> >> of sharing the `Type` representation with `TcType`, since the
> >> `coreView` function also has code to look through type synonyms.
> >>
> >> What is the reason for this? I would have expected type synonyms to be
> >> only relevant during typechecking, and then fully resolved in the
> >> elaborated Core output. If that were the case, then a new version of
> >> `expand_syn` could live in `TcM` and take care of making these fresh
> >> metavariables.
> >>
> >> Beside this concrete question, taking a step back, I would also like
> >> to hear from people who know their way around this part of GHC, what
> >> they think about this and how they'd approach implementing it.
> >>
> >> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220722/7e7a7229/attachment.html>