termination for FDs and ATs

[Martin Sulzmann]

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