Re: [Haskell-cafe] (Un)termination of overloading resolution
On Mon, 2006-02-27 at 16:43 +0800, Martin Sulzmann wrote: > I was talking about *static* termination. Hence, the conditions > in the paper and the new one I proposed are of course incomplete. Just to clarify: by static you mean verifiable at instance definition time (i.e. under the open world assumption) whereas dynamic is when the instance is used (i.e. in a closed world)? Note that both are "static" from a programmer's point of view, but this terminology definitely makes sense here. > I think that's your worry, isn't it? There are reasonable > type-level programs which are rejected but will terminate for certain > goals. My worry are type-level programs which are rejected but will provably terminate for *all* goals. > I think what you'd like is that each instance specifies its own > termination condition which can then be checked dynamically. That depends on what you mean by specifying a termination condition. Suppose we want to solve C t1 ... tn = t. A possible rule might be: if while solving this we ever come up with the goal C u1 ... un = u, then the number of constructors in u1 ... un must be strictly less than the number of constructors in t1 ... tn. Something similar to this should guarantee termination but would still allow structural recursion on types. Note that this doesn't even have to be fully dynamic - it can be checked once per module by using instance declarations as generators, I think. > Possible but I haven't thought much about it. The simplest and most > efficient strategy seems to stop after n number of steps. Yes, but I don't really like that. Any n will be completely arbitrary and rule out perfectly good type-level programs for no good reason. For what it's worth, this is essentially what C++ does and people don't like it and seem to largely ignore the limit specified in the standard. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] (Un)termination of overloading resolution
I was talking about *static* termination. Hence, the conditions in the paper and the new one I proposed are of course incomplete. I think that's your worry, isn't it? There are reasonable type-level programs which are rejected but will terminate for certain goals. I think what you'd like is that each instance specifies its own termination condition which can then be checked dynamically. Possible but I haven't thought much about it. The simplest and most efficient strategy seems to stop after n number of steps. Martin Roman Leshchinskiy writes: > On Mon, 27 Feb 2006, 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] > > Ah, sorry, my question was very poorly worded. What I meant to say was > that there are no instances declarations for C which satisfy your rule > above and, hence, all instances of C (or of any other class with > bidirectional dependencies) must satisfy the other, more restrictive > conditions. Is that correct? > > > In your example below, you are not only breaking the Bound Variable > > Condition, but you are also breaking the Coverage Condition. > > Yes, but I'm breaking the rule you suggested only once :-) It was only > intended as a cute example. My worry, however, is that there are many > useful type-level programs similar to my example which are guaranteed to > terminate but which nevertheless do not satisfy the rules in your paper or > the one you suggested here. I think ruling those out is unavoidable if you > want to specify termination rules which every instance must satisfy > individually. But why not specify rules for sets of instances instead? > This is, for instance, what some theorem provers do for recursive > functions and it allows them to handle a wide range of those without > giving up decidability. > > Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] (Un)termination of overloading resolution
On Mon, 27 Feb 2006, 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] Ah, sorry, my question was very poorly worded. What I meant to say was that there are no instances declarations for C which satisfy your rule above and, hence, all instances of C (or of any other class with bidirectional dependencies) must satisfy the other, more restrictive conditions. Is that correct? In your example below, you are not only breaking the Bound Variable Condition, but you are also breaking the Coverage Condition. Yes, but I'm breaking the rule you suggested only once :-) It was only intended as a cute example. My worry, however, is that there are many useful type-level programs similar to my example which are guaranteed to terminate but which nevertheless do not satisfy the rules in your paper or the one you suggested here. I think ruling those out is unavoidable if you want to specify termination rules which every instance must satisfy individually. But why not specify rules for sets of instances instead? This is, for instance, what some theorem provers do for recursive functions and it allows them to handle a wide range of those without giving up decidability. Roman ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] (Un)termination of overloading resolution
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 a
Re: [Haskell-cafe] (Un)termination of overloading resolution
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.
In general, wouldn't it be better to look at *all* visible instance
declarations when they are used instead of looking at each one
individually when it is defined? If the goal is to allow only primitive
recursion, then that would lead to much more permissive rules.
As to the non-termination of GHC's type checker, below is an example
which encodes a stripped-down version of the lambda calculus (with only
one variable) and then evaluates (\x. x x) (\x. x x). Loops nicely with
GHC 6.4.1, but the second Subst instance is invalid under your rule if I
understand correctly.
Roman
{-# 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')
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
x = undefined :: Eval (App (Lam (App X X)) (Lam (App X X))) u => u
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] (Un)termination of overloading resolution
On Tue, Feb 21, 2006 at 07:13:17PM -0800, [EMAIL PROTECTED] wrote: > I'm afraid that may still be insufficient, as the following > counter-example shows. It causes GHC 6.4.1 to loop in the typechecking > phase. I haven't checked the latest GHC. The HEAD is more cautious: F.hs:12:0: Variable occurs more often in a constraint than in the instance head in the constraint: E m a b (Use -fallow-undecidable-instances to permit this) In the instance declaration for `Foo m (a -> ())' This is required for all instances. GHC 6.4 relaxed it in the presence of FDs on the classes in the context, but as you've shown that is dangerous. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
[EMAIL PROTECTED] writes: > > Martin Sulzmann wrote: > > > Let's consider the general case (which I didn't describe in my earlier > > email). > > 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 > > ... > > > Sorry, I left out the precise definition of the rank function > > in my previous email. Here's the formal definition. > > > > rank(x) is some positive number for variable x > > > > rank(F t1 ... tn) = 1 + rank t1 + ... + rank tn > > > > where F is an n-ary type constructor. > > > > rank (f t) = rank f + rank t > > > > f is a functor variable > > Yes, I was wondering what rank means exactly. But now I do > have a problem with the criterion itself. The following simple and > quite common code > > > newtype MyIOState a = MyIOState (Int -> IO (a,Int)) > > > > instance Monad MyIOState where > > return x = MyIOState (\s -> return (x,s)) > > > > instance MonadState Int MyIOState where > > put x = MyIOState (\s -> return ((),x)) > > > becomes illegal then? Indeed, the class |MonadState s m| has a > functional dependency |m -> s|. In our case, > m = MyIOState, rank MyIOState = 1 > s = Intrank Int = 1 > and so rank(m) > rank(s) is violated, right? > > The additional conditions I propose are only necesssary once we break the Bound Variable Condition. Recall: The Bound Variable Condition (BV Condition) says: for each instance C => TC ts we have that fv(C) subsetof fv(ts) (the same applies to (super)class declarations which I leave out here). The above MonadState instance does NOT break the BV Condition. Hence, everything's fine here, the FD-CHR results guarantee that type inference is sound, complete and decidable. Though, your earlier example breaks the BV Condition. > class Foo m a where > foo :: m b -> a -> Bool > > instance Foo m () where > foo _ _ = True > > instance (E m a b, Foo m b) => Foo m (a->()) where > foo m f = undefined > > class E m a b | m a -> b where > tr :: m c -> a -> b > instance E m (() -> ()) (m ()) In the second instance, variable b appears only in the context but not in the instance head. But variable b is "captured" by the constraint E m a b where m and a appear in the instance head and we have that class E m a b | m a -> b. We say that this instance satisfies the Weak Coverage Condition. The problem is that Weak Coverage does not guarantee termination. See this and the earlier examples we have discussed so far. To obtain termination, I propose to impose stronger conditions on improvement rules (see above). My guess is that thus we obtain termination. If we can guarantee termination, we know that Weak Coverage guarantees confluence. Hence, we can restore sound, complete and decidable type inference. > BTW, the above definition of the rank is still incomplete: it doesn't say > what rank(F t1 ... tm) is where F is an n-ary type constructor and > m < n. Hopefully, the rank of an incomplete type application is bounded > (otherwise, I have a non-termination example in mind). If the rank is > bounded, then the problem with defining an instance of MonadState > persists. For example, I may wish for a more complex state (which is > realistic): > > > newtype MyIOState a = MyIOState (Int -> IO (a,(Int,String,Bool))) > > instance MonadState (Int,String,Bool) MyIOState > > Now, the rank of the state is 4... > The simple solution might be for any n-ary type constructor F rank(F t1 ... tm) = 1 + rank t1 + ... + rank tm where m<=n This might be too naive, I don't know. I haven't thought about the case where we need to compute the rank of a type constructor. Though, the style of termination proof I'm using dates back to Prolog which we know is untyped. Hence, there might not be any problem after all? Martin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
Martin Sulzmann wrote: > Let's consider the general case (which I didn't describe in my earlier > email). > 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 ... > Sorry, I left out the precise definition of the rank function > in my previous email. Here's the formal definition. > > rank(x) is some positive number for variable x > > rank(F t1 ... tn) = 1 + rank t1 + ... + rank tn > > where F is an n-ary type constructor. > > rank (f t) = rank f + rank t > > f is a functor variable Yes, I was wondering what rank means exactly. But now I do have a problem with the criterion itself. The following simple and quite common code > newtype MyIOState a = MyIOState (Int -> IO (a,Int)) > > instance Monad MyIOState where > return x = MyIOState (\s -> return (x,s)) > > instance MonadState Int MyIOState where > put x = MyIOState (\s -> return ((),x)) becomes illegal then? Indeed, the class |MonadState s m| has a functional dependency |m -> s|. In our case, m = MyIOState, rank MyIOState = 1 s = Intrank Int = 1 and so rank(m) > rank(s) is violated, right? BTW, the above definition of the rank is still incomplete: it doesn't say what rank(F t1 ... tm) is where F is an n-ary type constructor and m < n. Hopefully, the rank of an incomplete type application is bounded (otherwise, I have a non-termination example in mind). If the rank is bounded, then the problem with defining an instance of MonadState persists. For example, I may wish for a more complex state (which is realistic): > newtype MyIOState a = MyIOState (Int -> IO (a,(Int,String,Bool))) > instance MonadState (Int,String,Bool) MyIOState Now, the rank of the state is 4... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
[EMAIL PROTECTED] writes: > > > Let's consider the general case (which I didn't describe in my earlier > > email). > > > > 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 didn't know what condition you meant for the general form. But the > condition above is not sufficient either, as a trivial modification of the > example shows. The only modification is > > instance E ((->) (m ())) (() -> ()) (m ()) where > > and > test = foo (undefined::((() -> ()) -> ()) -> ()) (\f -> (f ()) :: ()) > > Now we have t1 = ((->) (m ())) : two constructors, one variable > t2 = () -> (): three constructors > t = m (): one constructor, one variable > > and yet GHC 6.4.1 loops in the typechecking phase as before. rank (() ->()) > rank (m ()) does NOT hold. Sorry, I left out the precise definition of the rank function in my previous email. Here's the formal definition. rank(x) is some positive number for variable x rank(F t1 ... tn) = 1 + rank t1 + ... + rank tn where F is an n-ary type constructor. rank (f t) = rank f + rank t f is a functor variable Hence, rank (()->()) = 3 rank (m ()) = rank m + 1 We cannot verify that 3 > rank m + 1. So, I still claim my conjecture is correct. Martin P. S. Oleg, can you next time please provide more details why type inference does not terminate. This will help others to follow our discussion. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
> Let's consider the general case (which I didn't describe in my earlier > email). > > 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 didn't know what condition you meant for the general form. But the condition above is not sufficient either, as a trivial modification of the example shows. The only modification is instance E ((->) (m ())) (() -> ()) (m ()) where and test = foo (undefined::((() -> ()) -> ()) -> ()) (\f -> (f ()) :: ()) Now we have t1 = ((->) (m ())) : two constructors, one variable t2 = () -> (): three constructors t = m (): one constructor, one variable and yet GHC 6.4.1 loops in the typechecking phase as before. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
This is not a counter-example to my conjecture.
Let's consider the general case (which I didn't
describe in my earlier email).
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
Your example violates this condition
> class E m a b | m a -> b
> instance E m (() -> ()) (m ())
The improvement rule says:
rule E m (() -> ()) x ==> x=(m ())
but rank m < rank (m ())
Your example shows that the condition
rank(t1)+...+rank(tn) > rank(t)
is not sufficient (but that's not a surprise).
Program text
> test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
gives rise to
Foo ((->) (() -> ())) ((() -> ()) -> ())
via
> instance (E m a b, Foo m b) => Foo m (a->()) where
this constraint reduces to
E ((->) (() -> ())) (()->()) x
Foo ((->) (() -> ())) x
the above improvement yields x = (((->) (() -> ( ()
this leads to
Foo ((->) (() -> ())) ->) (() -> ( ())
and so on (the second component is increasing).
So, I'll stick to my claim. I don't think I have time
at the moment to work out the details of my claim/proof sketch.
But if somebody is interested. The following is a good
reference how to attack the problem:
@inproceedings{thom-term,
author = "T. Fr{\"u}hwirth",
title = "Proving Termination of Constraint Solver Programs",
booktitle = "Proc.\ of New Trends in Constraints: Joint
{ERCIM/Compulog} Net
Workshop",
volume = "1865",
series = "LNAI",
publisher = "Springer-Verlag",
year = "2000"
}
Martin
[EMAIL PROTECTED] writes:
>
> Martin Sulzmann wrote:
>
> > - 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.
> >
> > Is there a possible fix? Here's a guess.
> > For each type definition in the AT case
> >
> > type T t1 = t2
> >
> > (or improvement rule in the FD case
> >
> > rule T1 t1 a ==> a=t2
> >
> > we demand that the number of constructors in t2
> > is strictly smaller than the in t1
> > (plus some of the other usual definitions).
>
> I'm afraid that may still be insufficient, as the following
> counter-example shows. It causes GHC 6.4.1 to loop in the typechecking
> phase. I haven't checked the latest GHC. The example corresponds to a
> type function (realized as a class E with functional dependencies) in
> the context of an instance. The function in question is
>
> class E m a b | m a -> b
> instance E m (() -> ()) (m ())
>
> We see that the result of the function, "m ()" is smaller (in the
> number of constructors) that the functions' arguments, "m" and
> "() -> ()" together. Plus any type variable free in the result is also
> free in at least one of the arguments. And yet it loops.
>
>
>
> {-# OPTIONS -fglasgow-exts #-}
> -- Note the absence of the flag -fallow-undecidable-instances
>
> module F where
>
> class Foo m a where
> foo :: m b -> a -> Bool
>
> instance Foo m () where
> foo _ _ = True
>
> instance (E m a b, Foo m b) => Foo m (a->()) where
> foo m f = undefined
>
> class E m a b | m a -> b where
> tr :: m c -> a -> b
>
> -- There is only one instance of the class with functional dependencies
> instance E m (() -> ()) (m ()) where
> tr x = undefined
>
> -- GHC(i) loops
>
> test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] (Un)termination of overloading resolution
Martin Sulzmann wrote:
> - 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.
>
> Is there a possible fix? Here's a guess.
> For each type definition in the AT case
>
> type T t1 = t2
>
> (or improvement rule in the FD case
>
> rule T1 t1 a ==> a=t2
>
> we demand that the number of constructors in t2
> is strictly smaller than the in t1
> (plus some of the other usual definitions).
I'm afraid that may still be insufficient, as the following
counter-example shows. It causes GHC 6.4.1 to loop in the typechecking
phase. I haven't checked the latest GHC. The example corresponds to a
type function (realized as a class E with functional dependencies) in
the context of an instance. The function in question is
class E m a b | m a -> b
instance E m (() -> ()) (m ())
We see that the result of the function, "m ()" is smaller (in the
number of constructors) that the functions' arguments, "m" and
"() -> ()" together. Plus any type variable free in the result is also
free in at least one of the arguments. And yet it loops.
{-# OPTIONS -fglasgow-exts #-}
-- Note the absence of the flag -fallow-undecidable-instances
module F where
class Foo m a where
foo :: m b -> a -> Bool
instance Foo m () where
foo _ _ = True
instance (E m a b, Foo m b) => Foo m (a->()) where
foo m f = undefined
class E m a b | m a -> b where
tr :: m c -> a -> b
-- There is only one instance of the class with functional dependencies
instance E m (() -> ()) (m ()) where
tr x = undefined
-- GHC(i) loops
test = foo (\f -> (f ()) :: ()) (\f -> (f ()) :: ())
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
