> > 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 <ge...@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.peytonjo...@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ő <ge...@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@haskell.org > >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > > > > _______________________________________________ > > ghc-devs mailing list > > ghc-devs@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs