termination for FDs and ATs
Simon PeytonJones
simonpj at microsoft.com
Thu May 4 09:00:33 EDT 2006
 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.
Actually, it won't. The spec just says that the function is monomorphic
in 'a'. That is, 'a' can be instantiated only one way. So if f is
called, say (f True True), then that fixes 'a' to be Bool and all is
well. Only if f is exported (with no calls inside the module) will the
program be rejected, and even then it'll be rejected on the grounds that
'a' is ambiguous.
But these are details. Your general point is well taken: the FD
improvement rule will infer
f :: Bool > Bool > Bool
without seeing any calls.
Simon
More information about the Haskellprime
mailing list