GHC and type-family rewriting?

[Benjamin Redelings]

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 <benjamin.redelings at gmail.com> 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