Claus Reinke wrote:
I hadn't given that much thought before, because FDs are meant to determine their range types, and there isn't much difference between universal and existential quantification if there is only one possible variable value, eg:
(forall a in {Char}. T a) vs (exists a in {Char}. T a)
That is quite an interesting issue, and the one on which different Haskell implementations differ. Let us consider the following code
{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-}
module Foo where
class C a b | a -> b, b -> a where foo :: b -> Bool
data E a = forall b. C a b => E b data U a = U (forall b. C a b => b)
We see that given the constraint "C a b", the type |a| unambiguously determines the type |b|, and vice versa. One may ask if the type |E a| provides any type abstraction over |b|, and if the type |U a| provides any generalization over |b|. Hugs (March 2005) and GHC 6.4.1 differ in their answers.
instance C a a where foo _ = True
t1 () = E undefined t1' = case t1 () of E x -> foo x
t2 () = U undefined t2' = case t2 () of U x -> foo x
Hugs -98 accepts this code; both t1' and t2' evaluate to True. GHC accepts t1 but flags t1'. GHC does not accept even t2. If we have more specific instances, then Hugs too reject the program (alas, for a different reason: unresolved overloading). If we have more specific instances
instance C () () where foo _ = True instance C [a] [a] where foo _ = False
then t2 becomes acceptable to GHC. t1' and t2' still present the problem; the latter is due to the unresolved overloading, which we can fix
t2 () = U undefined t2' = case t2 () of U x -> foo (tail x)
and now this code works in GHC, and Hugs. In Hugs, even the following is accepted:
t1 () = E () t1' () = case t1 () of E x -> foo x
however the inferred type for t1' is Foo> :t t1' t1' :: C a ([b] -> Bool) => () -> Bool which I can't explain at all... The slight change in the class:
class C a b | a -> b, b -> a where foo :: b -> a -> Bool
(please note: only the signature of foo is changed; the constraints and FD remain the same) the more specific instances now work in Hugs
instance C () () where foo _ _ = True instance C [a] [a] where foo _ _ = False
t1 () = E () t1' = case t1 () of E x -> foo x ()
t2 () = U undefined t2' = case t2 () of U x -> foo x []
As before, GHC accepts both t2 and t2' (but not t1'). It would be really great if the writers of typeclass-based programs could expect consistent results...
he suggested that the whole problem may be an instance of generalised propagation:
Generalised Constraint Propagation Over the CLP Scheme, by Thierry Le Provost and Mark Wallace. Journal of Logic Programming 16, July 1993. Also [ECRC-92-1] http://eclipse.crosscoreop.com:8080/eclipse/reports/ecrc_genprop.ps.gz
Francois Pottier's ICFP'05 invited talk had essentially the same gist: constraint propagation. He considered different domain: GADT and related implication and disequality constraints (I think he mentioned that the results applied to FDs as well) http://para.inria.fr/~fpottier/slides/fpottier-2005-09-icfp.pdf