# Reasoning backwards with type families

David Feuer david at well-typed.com
Thu Nov 16 01:31:55 UTC 2017

```Sometimes it woulld be useful to be able to reason backwards about type families.
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 either of the arguments, we can choose an equation and
learn something about the result. But if we know something about the *result*, GHC doesn't
give us any way to learn anything about the arguments. For (&&), the obvious things you'd
want are

prj1 :: (a && b) ~ 'True => a :~: 'True
prj2 :: (a && b) ~ 'True => b :~: 'True
flop :: (a && b) ~ 'False => (Not a || Not B) :~: 'True

constraint  (a && b) ~ 'True to hold, the type family application *must have reduced*
using one of its equations. The only possibilities are

'True && b = b
a && 'True = a
a && a = a

Substituting 'True for each RHS gives

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

So in each case, the first argument is forced to 'True.

Similarly, if (a && b) ~ 'False, we look at all the possibilities:

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

Substituting 'False for each RHS,

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

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

Now consider (==), which is recursive:

type family (a :: k) == (b :: k) :: Bool where
f a == g b = f == g && a == b
a == a = 'True
_ == _ = 'False

We'd really like to know that

eqEqual :: (a == b) ~ 'True => a :~: b
::
For eqEqual, we can reason thus: if  (a == b) ~ 'True, then we obtained that
result from one of the equations

f a == g b = f == g && a == b
a == a = 'True

In the base case, a ~ a on the LHS. In the recursive case, the RHS being 'True
tells us (using the reasoning for (&&)) that  (f == g) ~ True and that
(a == b) ~ True. Inductively, we conclude that f :~: g and a :~: b. Shifting
to the LHS, we conclude that f a ~ g b.

I wouldn't necessarily expect GHC to be able to work something like this out on
its own. But it seems like there should be some way to allow the user to guide
it to a proof. A tantalizing feature is that we're essentially reasoning about
execution traces, which are necessarily finite. It at least *seems* that this
should mean that the induction is well-founded. Now why should anyone