Ross Paterson writes: > Thanks for clarifying this. > > On Sat, Apr 29, 2006 at 05:49:16PM -0400, Manuel M T Chakravarty wrote: > > So, we get the following type for f > > > > f :: (Mul a b, [Result a b] = b) => Bool -> a -> b -> [Result a b] > > > > Given the instance definitions of that example, you can never satisfy > > the equality [Result a b] = b, and hence, never apply the function f. > > That would be the case if the definition were > > f b x y = if b then x .*. [y] else y > > You'd assign f a type with unsatisfiable constraints, obtaining > termination by deferring the check. But the definition > > f = \ b x y -> if b then x .*. [y] else y > > will presumably be rejected, because you won't infer the empty context > that the monomorphism restriction demands. So the MR raises the reverse > question: can you be sure that every tautologous constraint is reducible? > > > So, clearly termination for ATs and FDs is *not* the same. It's quite > > interesting to have a close look at where the difference comes from. > > The FD context corresponding to (*) above is > > > > Mul a [b] b > > > > Improvement gives us > > > > Mul a [[c]] [c] with b = [c] > > > > which simplifies to > > > > Mul a [c] c > > > > which is where we loop. The culprit is really the new type variable c, > > which we introduce to represent the "result" of the type function > > encoded by the type relation Mul. So, this type variable is an artifact > > of the relational encoding of what really is a function, > > It's an artifact of the instance improvement rule, but one could define > a variant of FDs without that rule. Similarly one could have a variant > of ATs that would attempt to solve the equation [Result a b] = b by > setting b = [c] for a fresh variable c. In both cases there is the > same choice: defer reduction or try for more precise types at the risk > of non-termination for instances like these. >
I agree. At one stage, GHC (forgot which version) behaved similarly compared to Manuel's AT inference strategy. Manuel may have solved the termination problem (by stopping after n number of steps). Though, we still don't know yet whether the constraints are consistent. One of the reasons why FD *and* AT inference is tricky is because inference may be non-terminating although - type functions/FD improvements are terminating - type classes are terminating We'll need a more clever analysis (than a simple occurs check) to reject 'dangerous' programs. Martin _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://haskell.org/mailman/listinfo/haskell-prime