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
There's nothing inherently impossible about this sort of reasoning. In order for the
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
care about this sort of business? Because the runtime representation of, say,
(a == b && c /= d) :~: 'True is smaller than the runtime representation of
(a :~: b, c :~: d -> Void). So it would be nice to be able to recover the latter
from the former. Can we do it?
David
More information about the ghc-devs
mailing list