[was ghc-devs] Reasoning backwards with type families

[Anthony Clayden]

> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote:

(Moving to ghc-users, there's nothing particularly dev-y.)

> Sometimes it woulld be useful to be able to reason
backwards
> about type families.

Hi David, this is a well-known issue/bit of a sore.
Discussed much in the debate between type families
compared to FunDeps.

> For example, we have
>
> type family a && b where
>   'False && b      = 'False
>   'True  && b      = b
>   a      && 'False = 'False
>   a      && 'True  = a
>   a      && a      = a

> ... if we know something about the *result*,
> GHC doesn't give us any way to learn anything about the
arguments.

You can achieve the improvement you want today.

You'll probably find Oleg has a solution
With FunDeps and superclass constraints, it'll go like this

class (OnResult r a b, OnResult r b a) => And a b r | a b ->
r

instance And 'False b 'False
-- etc, as you'd expect following the tf equations
-- the instances are overlapping but confluent

class OnResult r a b | r a -> b
instance OnResult 'True a 'True
instance OnResult 'False 'True 'False

You could equally make `OnResult` a type family.

If you can trace backwards to where `&&` is used,
you might be able to add suitable constraints there.

So there's a couple of futures:
* typechecker plugins, using an SMT solver
* injective type families
   the next phase is supposed to allow

type family a && b = r | r a -> b, r b -> a where ...

That will help with some type families
(such as addition of Nats),
plug1
https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#injective-type-families

but I don't see it helping here.
plug2 (this example)
https://github.com/AntC2/ghc-proposals/blob/instance-apartness-guards/proposals/0000-instance-apartness-guards.rst#type-family-coincident-overlap

Because (for example) if you unify the first two equations,
(that is, looking for coincident overlap)

    'False && 'False = 'False
    'True && 'False = 'False

That's inconsistent on dependency ` r b -> a`.

And you can't fix it by re-ordering the closed equations.

> 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 wouldn't necessarily expect GHC
> to be able to work something like this out on its own.

That's a relief ;-)

> But it seems like there should be some way to allow the
user
> to guide it to a proof.

Yes, an SMT solver with a model for kind `Bool`.
(And a lot of hard work to teach it, by someone.)

AntC