termination for FDs and ATs
Simon PeytonJones
simonpj at microsoft.com
Thu May 4 09:22:54 EDT 2006
This has been an interesting thread, starting here
http://www.haskell.org//pipermail/haskellprime/2006April/001466.html
Here is what I conclude so far.
1. As Manuel explained, in the AT formulation it's possible to avoid
nontermination 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/haskellprime/2006April/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 unqualified 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 instanceimprovement CHR arising
from the corresponding FD. But we can't drop the instanceimprovement
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* nontermination is thereby
eliminated from the ATinference 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/haskellprime/2006May/001514.html
Simon
 Original Message
 From: haskellprimebounces at haskell.org
[mailto:haskellprimebounces at haskell.org] On Behalf Of
 Ross Paterson
 Sent: 03 May 2006 09:37
 To: haskellprime 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 nonempty, 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.)

 _______________________________________________
 Haskellprime mailing list
 Haskellprime at haskell.org
 http://haskell.org/mailman/listinfo/haskellprime
More information about the Haskellprime
mailing list