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.
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
