[Haskell-cafe] Re:

[Martin Sulzmann]

On Wed, Oct 14, 2009 at 7:33 AM, <oleg at okmij.org> wrote:

>
> 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.


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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20091014/4088d9bc/attachment.html