FD improvement, variable quantification & generalised propagation

[oleg at pobox.com]

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