termination for FDs and ATs
sulzmann at comp.nus.edu.sg
Tue May 2 00:31:05 EDT 2006
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
More information about the Haskell-prime