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

_______________________________________________

ghc-devs mailing list

[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs