[Haskell] Re: Functional dependencies interfere with generalization

[oleg at pobox.com]

I'm sorry to open an old wound. I've just had an insight for
a clarification.

On Nov 26, 2003 Ken Shan wrote:

> Consider the following code, which uses type classes with functional
> dependencies:
>
>     {-# OPTIONS -fglasgow-exts #-}
>     module Foo where
>     class R a b | a -> b where r :: a -> b
>
>     -- 1
>     rr :: (R a b1, R a b2) => a -> (b1, b2)
>     rr a = (r a, r a)
>
>     -- 2
>     data RAB a = RAB (forall b. (R a b) => (a, b))
>     mkRAB :: (R a b) => a -> b -> RAB a
>     mkRAB a b = RAB (a, b)
>
> Neither 1 nor 2 passes the type-checker (GHC 6.0.1).  The error messages
> are similar:
>     Inferred type is less polymorphic than expected
>         Quantified type variable `b2' is unified with another
>         quantified type variable
>     When trying to generalise the type inferred for `rr'
>         Signature type:     forall a b1 b2.
>                             (R a b1, R a b2) =>
>                             a -> (b1, b2)
>         Type to generalise: a -> (b1, b1)

> In both cases, the compiler is failing to make use of functional
> dependencies information that it has at its disposal.  Specifically,
> it seems to me that, if two type variables b1 and b2 have been unified
> due to functional dependencies, making two constraints in the context
> identical, then the inner constraint ("inner" with respect to the scope
> of quantified type variables) should be ignored.

Regarding the function rr, I'm afraid I'm compelled to side with the
typechecker. It appears that the typechecker does make use of the
functional dependencies to reject the code because the user has
specified too general a signature. Exactly the _same_ error occurs in
the following code

	ab:: a -> Maybe a
	ab = Just

	rrr:: a -> (Maybe a, Maybe a1)
	rrr a = (ab a, ab a)

    Inferred type is less polymorphic than expected
        Quantified type variable `a1' is unified with another
	quantified type variable `a'
    When trying to generalise the type inferred for `rrr'
        Signature type:     forall a a1. a -> (Maybe a, Maybe a1)
        Type to generalise: a1 -> (Maybe a1, Maybe a1)
    When checking the type signature for `rrr'
    When generalising the type(s) for `rrr'

Error messages are identical.

Because ab is a function rather than a method, there trivially is a
functional dependency between the function's argument and its result.

Furthermore, exactly the same error occurs in

	rrrr:: a -> b
	rrrr x = x

    Inferred type is less polymorphic than expected
        Quantified type variable `b' is unified with
	another quantified type variable `a'
    When trying to generalise the type inferred for `rrrr'
        Signature type:     forall a b. a -> b
        Type to generalise: b -> b
    When checking the type signature for `rrrr'
    When generalising the type(s) for `rrrr'


Regarding the original function rr, the best solution seems to be to
let the compiler figure out its type. It seems in these circumstances
the most general type exists -- and thus the compiler can figure it
out.

Now, regarding function mkRAB. It seems there is a simple solution:

	data RAB a = RAB (forall b. (R a b) => (a, b))
	mkRAB a = RAB (a, r a)

Indeed, the class R a b promised that there is a function 'r' such
that given a value of type 'a' can produce a value of type 'b'. So, we
can make use of such a function.

One can object: in a value of a type RAB (forall b. (R a b) => (a, b)),
the types of two components of a pair `(a, b)' must be related by the
relation R a b. The values can in principle be arbitrary. What if one
wishes to create a value RAB (x,z) such that the value z has the type of
(r x) but is not equal to (r x)? Well, there is an underhanded way to
help that.

	class R a b | a -> b where 
	   r ::  a -> b
	   r1 :: a -> Integer -> b

that is, we define an additional method that takes an integer and
somehow makes the value of a type 'b'. We may imagine an Array(s) of all
possible values of type 'b' (specialized for those types 'b' for which
there are instances of the class R) and the method r1 merely uses its
second argument to select from that array. In any case, Goedel showed
that quite many pleasant and unpleasant things can be encoded in
integers. The first argument of r1 is merely a window dressing to
make the typechecker happy.

Thus we can define

	mkRAB' a b = RAB (a, r1 a b)

To make the code more concrete, we introduce two instances

instance R Int Char where {r = toEnum; r1 _ = toEnum . fromInteger}
instance R Float (Maybe Float) where
    r = Just
    r1 _ 1 = Nothing
    r1 _ n = Just (fromRational $ toRational (n-1) / (2^(128+1)))
    

In the second instances, we take advantage of the existence of an
injection from IEEE floating-point numbers to integers.

We can try evaluating "mkRAB 65", "mkRAB' 65 66", "mkRAB' (1.0::Float)
0", etc. -- and everything works.

Building RAB values is not enough -- we should be able to use
them. For example, we should be able to define the following function

    useRAB :: (Eq b, R a b) => RAB a -> b -> Bool
    useRAB (RAB (a, b1)) b2 = b1 == b2

As Ken Shan pointed out on Nov 27, 2003, it doesn't type. But the
following does:

	useRAB (RAB x) b2 = (snd x) == b2

If we ask the typechecker to give us the type of useRAB, it says:

	*Foo> :t useRAB
	useRAB :: forall b a. (R a b, Eq b) => RAB a -> b -> Bool

which is _precisely_ as we wished. It all seems to work:

*Foo> useRAB (mkRAB (65::Int)) 'a'
False
*Foo> useRAB (mkRAB (65::Int)) 'A'
True
*Foo> useRAB (mkRAB (65::Int)) 'B'
False
*Foo> useRAB (mkRAB' (65::Int) 66) 'B'
True
*Foo> useRAB (mkRAB (1.0::Float)) (Just (1.0::Float))
True
*Foo> useRAB (mkRAB' (1.0::Float) 1) Nothing            
True

	Am I missing something in the original problem?