[was ghc-devs] Reasoning backwards with type families

[Anthony Clayden]

On Thu, 14 Dec 2017 at 3:19 PM, David Feuer <redirect at vodafone.co.nz> wrote:

> I still haven't really digested what you've written, but I wish to pick a
> nit (below)
>

Thanks David. Heh, heh. I think we might be agreeing about the phenomenon,
but picking different nits to 'blame'.


> On Nov 20, 2017 3:44 AM, "Anthony Clayden" <anthony_clayden at clear.net.nz>
> wrote:
>
> > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:
>
> ...
>
>
>
> > For (&&), the obvious things you'd want are ...
> >
> > There's nothing inherently impossible about this sort of
> reasoning.
>
> No-ish but. It relies on knowing kind `Bool` is closed.
> And GHC doesn't pay attention to that.
> So you need to bring type family `Not`
> into the reasoning; hence a SMT solver.
>
>
> I don't think this is entirely correct. The fact that Bool is closed does
> not seem relevant.  The key fact, I believe, is that (&&) is closed.
>

Hmm. I wonder what you think "closed" amounts to?

Equation 1    `'False && b    = 'False` is consistent with `[b ~ Foo]`
   (unless GHC were to reason about closed kinds)

Equation 2    `'True  && b     = b   ` is consistent with `[b ~ Foo]`

And so on.

The last equation `a      && a    = a` is consistent with `[a ~ Foo]`.
Furthermore it's *inconsistent* with a putative backwards FunDep ` r a ->
b` on `'False && 'True ~ 'False`.
I think it would be better to omit that equation all together.

Then when your o.p. reasons:

>>> ... we can calculate (Not a || Not b) as 'True for each of these LHSes.

What will it calculate for (Not Foo)?

Asking GHC to reason like this about open type families smells much harder,
> but maybe my sense of smell is off.
>
> Hmm. Your o.p. said

>>> In order for the constraint (a && b) ~ 'True to hold, the type family
application *must have reduced* using one of its equations.

I think that's smelly logic: if you want to reason backwards, then you
can't make assumptions about what "must" have reduced if GHC were
reasoning forward. That is, unless you're expecting GHC to behave like
an SMT solver over closed kinds.

Remember that the logic for selecting Closed Type Family equations
works from top to bottom *ignoring anything known about the result*.
So not only must it have reduced using one of the equations; it must
have rejected equations above the one it selected; and it must have
seen evidence for rejecting them. (It's more complicated than that in
practice: if there's coincident overlap, GHC will pick some equation
eagerly. And your `&&` equations exhibit coincident overlap, apart
from the last.)

If you want it to benefit from something known about the result, you
won't (in general) find the same top-to-bottom sequence helps with
type improvement. With the FunDep inconsistency in your last equation
for `&&`, I suspect that equation-selection will get 'stuck' looking
for evidence to reject earlier equations.

If we do expect GHC to behave like an SMT solver over closed kinds,
then it can reason just as well for an open type family; on the
proviso that it can see all the equations.

For a bit of history: during discussions around Injective Type
Families, one suggestion was to infer injectivity by examining the
equations given -- along the lines you're positing. That was rejected
on grounds the equations might exhibit injectivity 'by accident'. Also
that the programmer might intend injectivity, but their equations be
inconsistent. So it was decided there must be explicit declaration;
and the equations must be consistent with that declaration. No
equations for `&&` could be consistent that way.

AntC
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20171214/1834fefb/attachment.html>