Martin Sulzmann wrote:
"Undecidable" instances means that there exists a program for which there's an infinite reduction sequence.
I believe this may be too strong of a statement. There exists patently terminating type families that still require undecidable instances in GHC. Here is an example:
{-# LANGUAGE TypeFamilies #-}
type family I x :: * type instance I x = x
type family B x :: * type instance B x = I x
GHC 6.8.3 complaints: Application is no smaller than the instance head in the type family application: I x (Use -fallow-undecidable-instances to permit this) In the type synonym instance declaration for `B' But there cannot possibly be any diverging reduction sequence here, can it? The type family I is the identity, and the type family B is its alias. There is no recursion. The fact that type families are open is not relevant here: our type families I and B are effectively closed, because one cannot define any more instance for I and B (or risk overlap, which is rightfully not supported for type families). The reason GHC complains is because it checks termination instance-by-instance. To see the termination in the above program, one should consider instances I and B together. Then we will see that I does not refer to B, so there are no loops. But this global termination check -- for a set of instances -- is beyond the abilities of GHC. This is arguably the right decision: after all, GHCi is not a full-blown theorem prover. Thus there are perfectly decidable type programs that require undecidable instances. Indeed, there is no reason to be afraid of that extension.
On Wed, Oct 14, 2009 at 7:33 AM,
"Undecidable" instances means that there exists a program for which
Martin Sulzmann wrote: there's
an infinite reduction sequence.
I believe this may be too strong of a statement. There exists patently terminating type families that still require undecidable instances in GHC.
Sorry, I wasn't precise enough. I didn't mean to say that *every* program which requires "undecidable" instance won't terminate. Rather, take any of the properties which imply decidability. Then, there *exists* a program which satisfies the negated property and this program won't terminate. As you show, for specific cases we can argue that "undecidable" instances are decidable. You can even argue that the Add/Mult example is decidable, assuming we never generate loopy type constraints. -Martin
Here is an example:
{-# LANGUAGE TypeFamilies #-}
type family I x :: * type instance I x = x
type family B x :: * type instance B x = I x
GHC 6.8.3 complaints: Application is no smaller than the instance head in the type family application: I x (Use -fallow-undecidable-instances to permit this) In the type synonym instance declaration for `B'
But there cannot possibly be any diverging reduction sequence here, can it? The type family I is the identity, and the type family B is its alias. There is no recursion. The fact that type families are open is not relevant here: our type families I and B are effectively closed, because one cannot define any more instance for I and B (or risk overlap, which is rightfully not supported for type families).
The reason GHC complains is because it checks termination instance-by-instance. To see the termination in the above program, one should consider instances I and B together. Then we will see that I does not refer to B, so there are no loops. But this global termination check -- for a set of instances -- is beyond the abilities of GHC. This is arguably the right decision: after all, GHCi is not a full-blown theorem prover.
Thus there are perfectly decidable type programs that require undecidable instances. Indeed, there is no reason to be afraid of that extension.
participants (2)
-
Martin Sulzmann -
oleg＠okmij.org