[Haskell] Re: Functional dependencies interfere with generalization
oleg at pobox.com
oleg at pobox.com
Wed Jan 28 22:47:16 EST 2004
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?
More information about the Haskell
mailing list