[Haskell-cafe] (Un)termination of overloading resolution
Martin Sulzmann
sulzmann at comp.nus.edu.sg
Sun Feb 26 23:23:21 EST 2006
The following not only answers Roman's question but
also includes a short summary (at the end) of the discussion
we had so far.
Roman Leshchinskiy writes:
> On Wed, 2006-02-22 at 12:33 +0800, Martin Sulzmann wrote:
> > In case we have an n-ary type function T
> > (or (n+1)-ary type class constraint T)
> > the conditions says
> > for each
> >
> > type T t1 ... tn = t
> >
> > (or rule T t1 ... tn x ==> t)
> >
> > then rank(ti) > rank(t) for each i=1,..,n
>
> I'm probably misunderstanding something but doesn't this imply that we
> cannot declare any instances for
>
> class C a b | a -> b, b -> a
>
> which do not break the bound variable condition? This would remove one
> of the main advantages fundeps have over associated types.
>
Sure you can. For example,
class C a b | a->b, b->a
instance C [a] [a]
The above class/instance declarations satisfy
the Consistency, Coverage, Basic Bound Variable Conditions.
See "Understanding FDs via CHRs" paper (see Sect 4, 4.1).
Under these conditions, we know that type inference is sound,
complete and decidable.
In your example below, you are not only breaking the Bound Variable
Condition, but you are also breaking the Coverage Condition.
> {-# OPTIONS -fglasgow-exts #-}
> data X
> data App t u
> data Lam t
>
> class Subst s t u | s t -> u
> instance Subst X u u
> instance (Subst s u s', Subst t u t') => Subst (App s t) u (App s'
t')
breaks Coverage
> instance Subst (Lam t) u (Lam t)
>
> class Apply s t u | s t -> u
> instance (Subst s t u, Eval u u') => Apply (Lam s) t u'
>
> class Eval t u | t -> u
> instance Eval X X
> instance Eval (Lam t) (Lam t)
> instance (Eval s s', Apply s' t u) => Eval (App s t) u
breaks Coverge and Bound Variable
>
> x = undefined :: Eval (App (Lam (App X X)) (Lam (App X X))) u => u
>
It's no surprise that the ghc inferencer does not terminate.
We know that breaking the Coverage Condition alone (not breaking
any of the other conditions) will break termination. Well, not
always but for certain examples.See Example 15, Sect 5.2 in the paper.
We also know that breaking the Bound Variable Condition will break
termination. See Example 16, Sect 5.2.
All this may be surprising, cause the instances are terminating.
It's the devious interaction between instance reduction and
improvement.
In case we break the Coverage Condition we need to find some "weaker"
conditons which guarantee confluence (i.e. complete inference)
*if* we know that inference is decidable. See Sect 6.
So, it's really termination that's the trouble maker and there's
really not hope to maintain termination in general. Though, if we can
verify termination, e.g. for a particular inference goal, we obtain
completeness. Hence, inference is sound, complete but semi-decidable.
How/why did we need up talking about decidable FD inference?
Well, somebody (can't remember who) asked how to translate the
following FD program to ATs.
class D b
class D b => C a b | a->b
In the AT system, FDs are expressed via type relations.
class D b
class D (T a) => C a where
type T a
The point here is that to encode the FD program the AT system
(as described in ICFP'05) needs to be extended. Specifically,
associated type synonyms may now constrain the types of
type classes in the instance/superclass context.
I've pointed out that this easily leads to undecidable type inference.
I've appended my *old email* below.
My main point were:
- The type functions are obviously terminating, e.g.
type T [a] = [[a]] clearly terminates.
- It's the devious interaction between instances/superclasss
and type function which causes the type class program
not to terminate.
The problem with decidable AT inference is very similar to the
FD case where we break the Bound Variable Condition.
Here's a "rough" FD encoding of the above AT program.
class T a b | a->b
class D b
class (D b, T a b) => C a
^^^^^^^^^^^
Notice that the superclass context contains the unbound variable b.
This observation allowed me to lift the "critical" FD examples to
the AT world.
As a remedy to the undecidability issue, I proposed to impose
stronger conditions on AT type relations (we know the AT type
relations are terminating but that's still not enough).
I'm not reproducing here the details, see my earlier emails.
Also note that similar conditions can be applied to FD programs
(to recover decidability).
Here's now the summary:
- Decidable type inference for ATs and FDs is an equally hard problem.
- There's a huge design space which additional conditions will recover
decidability, e.g. impose ranking conditions on type relations,
dynamic termination checks etc. It's very likely that similar
conditions apply to FDs and ATs.
- To encode certain FD programs the AT system needs extensions which
may threaten decidable type inference.
Martin
*old email*
> > Stefan Wehr writes:
> > > [...]
> > > Manuel (Chakravarty) and I agree that it should be possible to
> > > constrain associated type synonyms in the context of class
> > > definitions. Your example shows that this feature is actually
> > > needed. I will integrate it into phrac within the next few days.
> > >
> >
> > By possible you mean this extension won't break any
> > of the existing ATS inference results?
>
> Yes, although we didn't go through all the proofs.
>
> > You have to be very careful otherwise you'll loose decidability.
>
> Do you have something concrete in mind or is this a more general
> advice?
>
I'm afraid, I think there's a real issue.
Here's the AT version of Example 15 from "Understanding FDs via CHRs"
class D a
class F a where
type T a
instance F [a] where
type T [a] = [[a]]
instance (D (T a), F a) => D [a]
^^^^^^^
type function appears in type class
Type inference (i.e. constraint solving) for D [a] will not terminate.
Roughly,
D [[a]]
-->_instance D (T [a]), F [a])
-->_type function D [[a]], F [a]
and so on
Will this also happen if type functions appear in superclasses?
Let's see. Consider
class C a
class F a where
type T a
instance F [a] where
type T [a] = [[[a]]]
class C (T a) => D a
^^^^^
type function appears in superclass context
instance D [a] => C [[a]] -- satisfies Ross Paterson's Termination Conditions
Consider
D [a]
-->_superclass C (T [a]), D [a]
-->_type function C [[[a]]], D [a]
-->_instance D [[a]], D [a]
and so on
More information about the Haskell-Cafe
mailing list