> On Jan 6, 2020, at 05:29, Richard Eisenberg <r...@richarde.dev> wrote:
>
> 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.
Thanks, this all makes sense to me. I actually went back and re-read the
injective type families paper after responding to your previous email, and I
discovered it actually alludes to the issue we’re discussing! At the end of the
paper, in section 7.3, it provides the following example:
> Could closed type families move beyond injectivity and functional
> dependencies by applying closed-world reasoning that derives solutions of
> arbitrary equalities, provided a unique solution exists? Consider this
> example:
>
> type family J a where
> J Int = Char
> J Bool = Char
> J Double = Float
>
> One might reasonably expect that if we wish to prove (J a ∼ Float), we will
> simplify to (a ∼ Double). Yet GHC does not do this as neither injectivity nor
> functional dependencies can discover this solution.
This is not quite the same as what we’re talking about here, but it’s clearly
in the same ballpark.
I think what you’re describing makes a lot of sense, and it would be
interesting to explore what it would take to encode into core. After thinking a
little more on the topic, I think that probably makes by far the most sense
from the core side of things. But I agree it seems like a significant change,
and I don’t know enough about the formalism to know how difficult it would be
to prove soundness. (I haven’t done much formal proving of anything!)
Alexis
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
