termination for FDs and ATs

[Martin Sulzmann]

In more detail, here's the issue I see.

The AT inference system doesn't exhaustively apply all rules,
rather, the AT inferencer stops once we encounter a 'cycle'
such as T a = a where T is a type function constructor.

The important question is whether this will retain *complete* type
inference? For example, in case of type annotations we need to
test for equivalence among constraints.

In the "A Theory of Overlaoding" and FD-CHR paper we develop
a equivalence check by exhaustively applying rules
until we reach a canonical normal form. This check is complete
if the rules are terminating and confluent (roughly).

If the rules are non-terminating, we obviously can't apply
the rules exhaustively. Howver, then it's unclear whether
the equivalence check is still complete.

You'll need to convince me that the AT inferencer computes
canonical (?) normal forms which are good enough to obtain
a complete equivalence checker. My guess is that any positive
result in this direction suggests that we should have immediately
rejected a constraint such as T a = a in the first place.

Martin

Simon Peyton-Jones writes:
 > This has been an interesting thread, starting here
 > 	
 > http://www.haskell.org//pipermail/haskell-prime/2006-April/001466.html
 > 
 > Here is what I conclude so far.
 > 
 > 1.  As Manuel explained, in the AT formulation it's possible to avoid
 > non-termination by suspending (leave unsolved) any equality constraint
 > of form (a = ty) where 'a' appears free in a type argument to an
 > associated type in 'ty'.
 > 	
 > http://www.haskell.org//pipermail/haskell-prime/2006-April/001501.html
 > 
 > 2.  This solution is not the same as stopping after a fixed number N of
 > iterations.  It's more principled than that.  
 > 
 > 3.  We may thereby infer a type that can never be satisfied, so that the
 > function cannot be called.  (In Martin's vocabulary, "the constraints
 > are inconsistent".)  Not detecting the inconsistency immediately means
 > that error messages may be postponed.  Adding a type signature would fix
 > the problem, though.
 > 
 > 4.  As Ross shows below, we may thereby infer a qualified type when
 > there is a unique, completely un-qualified solution.  But that does
 > little harm, I think.  The only time you can even tell it has happened
 > is if (a) the defn falls under the MR (in particular, no type signature
 > is given), (b) the function is exported, and (c) it is not called inside
 > the module.
 > 
 > 5.  The effect is akin to dropping the instance-improvement CHR arising
 > from the corresponding FD.  But we can't drop the instance-improvement
 > CHR because then lots of essential improvement would fail to take place.
 > It is not obvious to me how to translate the rule I give in (1) into the
 > CHR framework, though doubtless it is possible.
 > 
 > 6.  I don't think we yet know whether *all* non-termination is thereby
 > eliminated from the AT-inference story.  Manuel and Martin and I are
 > starting to write down the formal story for an AT system that covers
 > both data types, type synonyms, and various other small extensions to
 > ATs, so we hope to find out soon.  (In this world, "small extensions"
 > are easy to describe, but sometimes have a big effect.  So formalising
 > it is important.)   
 > 
 > 7.  In particular, Martin writes "We'll need a more clever analysis
 > (than a simple occurs check) to reject
 > 'dangerous' programs."   But so far I don't see why we might need a more
 > clever analysis than the rule I describe in (1) above.  I'm not denying
 > that such a thing might exist, but I wonder if you have anything in
 > mind?
 > 	
 > http://www.haskell.org//pipermail/haskell-prime/2006-May/001514.html
 > 
 > Simon
 > 
 > 
 > | -----Original Message-----
 > | From: haskell-prime-bounces at haskell.org
 > [mailto:haskell-prime-bounces at haskell.org] On Behalf Of
 > | Ross Paterson
 > | Sent: 03 May 2006 09:37
 > | To: haskell-prime at haskell.org
 > | Subject: Re: termination for FDs and ATs
 > | 
 > | On Tue, May 02, 2006 at 12:26:48AM +0100, Ross Paterson wrote:
 > | > So the MR raises the reverse
 > | > question: can you be sure that every tautologous constraint is
 > reducible?
 > | 
 > | I think the answer is no.  Consider:
 > | 
 > | 	class C a where
 > | 		type Result a
 > | 		method :: a -> Result a
 > | 
 > | 	instance C (Maybe a) where {
 > | 		type Result (Maybe a) = Bool
 > | 
 > | 	f = \ b x -> if b then Just (method x) else x
 > | 
 > | The AT algorithm will stop after inferring the following type for f:
 > | 
 > | 	(a = Maybe (Result a), C a) => Bool -> a -> a
 > | 
 > | Since the constraint set is non-empty, this definition will be
 > rejected
 > | by the monomorphism restriction.
 > | 
 > | However, this constraint set has exactly the same set of solutions as
 > | a = Maybe Bool, which is trivially solvable.  (The corresponding FD
 > | version will reduce to this, thanks to instance improvement.)
 > | 
 > | _______________________________________________
 > | Haskell-prime mailing list
 > | Haskell-prime at haskell.org
 > | http://haskell.org/mailman/listinfo/haskell-prime
 > _______________________________________________
 > Haskell-prime mailing list
 > Haskell-prime at haskell.org
 > http://haskell.org/mailman/listinfo/haskell-prime