termination for FDs and ATs

[Simon Peyton-Jones]

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