Re: GHC and type-family rewriting?
> On Dec 17, 2022, at 10:17 AM, Benjamin Redelings > wrote: > > But supposing I do get there, I'm curious if there are some papers on > term-rewriting that would be helpful to set the context? The OutsideIn paper > mentions Kapur (1997) "Shostak's congruence closure as completion" in support > of the flattening idea. I'm not aware of any, but I think looking for some is a good idea. For better or worse, the current approach was freshly invented; looking for prior art might have yielded something better. Richard___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: GHC and type-family rewriting?
Hi Richard, Thanks! This context of where the current GHC approach came from is quite helpful. I think I see what you mean by reducing type families only in "strict" positions... and maybe I see what you mean by trying to make the whole approach less ugly. I still need to do quite a bit of plumbing work before I get to anything that interesting. But supposing I do get there, I'm curious if there are some papers on term-rewriting that would be helpful to set the context? The OutsideIn paper mentions Kapur (1997) "Shostak's congruence closure as completion" in support of the flattening idea. -BenRI On 12/8/22 11:48 PM, Richard Eisenberg wrote: On Nov 30, 2022, at 9:42 PM, Benjamin Redelings wrote: (Q1) Did GHC evolve to this point starting from something fairly close to the OutsideIn paper? Yes. (Q2) Is the new approach (i.e. eager type family rewriting) mostly to making rewriting faster? No. Simpler, not faster (and not slower). Or that was the intent. (Q3) Does it sound reasonable to implement the approach from the OutsideIn paper, and than gradually transform it to look more like GHC? Sure, but I'm not sure what the advantage of doing so would be. This is all my doing: for years and years, GHC's treatment of type families was as described in OutsideIn. But I never could quite figure out why we needed to have flattening variables. And so I got rid of them -- this seemed like a simplification. I'm not sure it really panned out, though: without flattening variables, we need these cycle-breaker variables (which are pretty gross). On the flip side, I think the new approach might enable the possibility of reducing type families only in "strict" positions (e.g. the argument to another type family or perhaps a class during instance lookup). In the end, I don't think either the old way or the new way is the Right Answer. Maybe you can come up with something better than both! Richard Thanks! This is quite helpful. -BenRI ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: GHC and type-family rewriting?
> On Nov 30, 2022, at 9:42 PM, Benjamin Redelings > wrote: > > (Q1) Did GHC evolve to this point starting from something fairly close to the > OutsideIn paper? Yes. > > (Q2) Is the new approach (i.e. eager type family rewriting) mostly to making > rewriting faster? No. Simpler, not faster (and not slower). Or that was the intent. > > (Q3) Does it sound reasonable to implement the approach from the OutsideIn > paper, and than gradually transform it to look more like GHC? > Sure, but I'm not sure what the advantage of doing so would be. This is all my doing: for years and years, GHC's treatment of type families was as described in OutsideIn. But I never could quite figure out why we needed to have flattening variables. And so I got rid of them -- this seemed like a simplification. I'm not sure it really panned out, though: without flattening variables, we need these cycle-breaker variables (which are pretty gross). On the flip side, I think the new approach might enable the possibility of reducing type families only in "strict" positions (e.g. the argument to another type family or perhaps a class during instance lookup). In the end, I don't think either the old way or the new way is the Right Answer. Maybe you can come up with something better than both! Richard > -BenRI > > ___ > 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 and type-family rewriting?
Hi, I've managed to code up implications and GADTs, and am now working on adding type families. I've been following the OutsideIn paper, but it seems that GHC is not really following the same plan for the solver. For example, instead of replacing every type family with a metavariable, it only does this for occur-check failures. It talks about "cycle breakers" instead of "flattening substitutions". It creates flatting substitutions for both givens and wanteds (I think). And I see this note: -- | A 'Xi'-type is one that has been fully rewritten with respect -- to the inert set; that is, it has been rewritten by the algorithm -- in GHC.Tc.Solver.Rewrite. (Historical note: 'Xi', for years and years, -- meant that a type was type-family-free. It does *not* mean this -- any more.) type Xi = TcType If I'm understanding correctly, the inert set is now thought of as a "generalized substitution" that replaces either an LHS (untouchable type variables or type family applications) with an RHS. I guess what I'm wondering is: (Q1) Did GHC evolve to this point starting from something fairly close to the OutsideIn paper? (Q2) Is the new approach (i.e. eager type family rewriting) mostly to making rewriting faster? (Q3) Does it sound reasonable to implement the approach from the OutsideIn paper, and than gradually transform it to look more like GHC? -BenRI ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
