Superclasses of type families returning constraints?

[Richard Eisenberg]

You're absolutely right that improvement doesn't solve your problem. But what I didn't say is that there is no real reason (I think) that we can't improve improvement to produce givens. This would likely require a change to the coercion language in Core (and thus not to be taken lightly), but if we can identify a class of programs that clearly benefits from that work, it is more likely to happen. The thoughts about improvement were just a very basic proof-of-concept. Sadly, the proof-of-concept failed, so I think a first step in this direction would be to somehow encode these partial improvements, and then work on changing Core. That road seems too long, though, so in the end, I think constrained type families (with superclass constraints) might be a more fruitful direction.

Richard

> On Jan 5, 2020, at 6:02 PM, Alexis King <lexi.lambda at gmail.com> wrote:
> 
>> On Jan 4, 2020, at 20:38, Richard Eisenberg <rae at richarde.dev> wrote:
>> 
>> I thought that, maybe, we could use partial improvement to give you what you want
> 
> I think that improvement alone cannot possibly be enough here, as improvement by its nature does not provide evidence. Improvement allows us to take a set of constraints like
> 
>    [G] FD2 a Bool
>    [W] FD2 a b
> 
> and derive [WD] b ~ Bool, but importantly this does not produce a new given! This only works if b is a metavariable, since we can solve the new wanted by simply taking b := Bool, but if b is rigid, we are just as stuck as before. In other words, improvement only helps resolve ambiguities, not derive any new information.
> 
> That’s why I think the “superclass” characterization is more useful. If instead we express your FD2 class as
> 
>    class b ~ B a => FD2 a b where
>      type B a
> 
> then if we have [G] FD2 a Bool, we can actually derive [G] B a ~ Bool, which is much stronger than what we were able to derive using improvement.
> 
> I imagine you are aware of all of the above already, but it’s not immediately clear to me from your description why you need functional dependencies (and therefore improvement) rather than this kind of approximation using superclasses and type families. Would modeling things with that approximation help at all? If not, why not? I think that would help me understand what you’re saying a little better.
> 
> Thanks,
> Alexis