Solved: Typing problems with polymorphic recursion and typeclasses
I think I can explain why Haskell compilers behave as they do with regards to Levent Erkok's problem, and how to fix it. It seems the compilers are more powerful than we imagine, but are compelled to conceal their power and to lie to us. First, let us distill the problem to the following few lines:
f:: (Show fa) => fb -> fa f = undefined
g:: (Show ga) => ga -> gb g = undefined
-- h:: (Show fa) => t -> fa h b = f (g (h b))
This code loads and checks. If we ask the compiler for the type of h, we get the type of h that was commented out in the code above. If we remove the comment and reload the code, we get an error: Ambiguous type variable(s) `fa' in the constraint `Show fa' arising from use of `h' at /tmp/p.lhs:12 In the first argument of `g', namely `(h b)' In the first argument of `f', namely `(g (h b))' This behavior seems rather puzzling: the compiler refuses to accept its own type. The problem is that the compiler is slightly lying to us. When we ask for the type *Main> :type h forall fa t. (Show fa) => t -> fa the real type of h is forall t. t -> (function-of-t) The real type of h is not totally polymorphic : it is dependent! It goes without saying that such types cannot be expressed in Haskell. It is stunning that the compiler managed to infer such a dependent type, albeit it has no way to properly print it. The compiler could have used the following notation: forall fa t | t -> fa. (Show fa) => t -> fa Perhaps even more stunning is that we can test our hypothesis. We can explicitly specify the functional dependence between types. We will use lexically-scoped type variables, described in the eponymous paper by Simon Peyton-Jones and Mark Shields. The following works in GHC 5.04.1, given -fglasgow-exts flag.
h1:: (Show t2) => t1 -> t2 h1 b :: g1a = (f (g ((h1 b)::g1a)))
Original example by Levent Erkok's also works.
Oleg writes:
the real type of h is forall t. t -> (function-of-t)
The real type of h is not totally polymorphic : it is dependent!
Ummm... that doesn't look like a dependent type to me, it looks like a functional dependency. A dependent type would be forall t. x::t -> (function-of-x) Perhaps it's not (quite) so surprising? --KW 8-)
First, let us distill the problem to the following few lines:
f:: (Show fa) => fb -> fa f = undefined
g:: (Show ga) => ga -> gb g = undefined
-- h:: (Show fa) => t -> fa h b = f (g (h b))
Here's a simplified version. h :: (Show ha) => t -> ha h b = g (h b) Same problem occurs. Though this is strange. Consider type inference for h b = g (h b) We generate the following constraints: th = tb -> ga, Show ga -- results from g (h b) th = tb -> gb -- taking into account h b = g (h b) In case of h :: (Show ha) => t -> ha h b = g (h b) we additionally generate th = t -> ha, Show ha Overall, we find th = tb -> ga, Show ga th = tb -> gb, th = t -> ha, Show ha (*) Note that this implies ga=ha, gb=ha The error message Ambiguous type variable(s) `ha' in the constraint `Show ha' arising from use of `g' at HaskellMay03.hs:16 In the definition of `h'': g (h' b) suggests that ghc does not apply the unifier ha=ga. I suspect the type computed out of the constraints from (*) is as follows: (Show ga, Show ha) => t -> ha Indeed hugs says ERROR HaskellMay03.hs:13 - Cannot justify constraints in explicitly typed binding *** Expression : h *** Type : Show a => b -> a *** Given context : Show a *** Constraints : Show c That is, the type (Show ga, Show ha) => t -> ha does not conform to the annotation (Show ha) => t -> ha. In case we use scoped type variables h2:: (Show t2) => t1 -> t2 h2 b :: g1a = g ((h2 b)::g1a) we impose some additional constraints (ga=g1a, ha=g1a). This seems to resolve the problem, though, as my above calculation shows there shouldn't be a problem in the first place. E.g. Chameleon accepts without problem h :: (Show ha) => t -> ha h b = g (h b) or h :: (Show ha) => t -> ha h b = g ((h b)::ha) This is the Chameleon equivalent to h2. Scoped type variables in Chameleon refer to type annotations. You can try this out by calling chameleon -d HaskellMay03.hs where HaskellMay03.hs = hconstraint Show -- Chameleon does not know the Prelude. -- We have to introduce type class constraints -- explicitely g:: (Show ga) => ga -> gb g = undefined h :: (Show ha) => t -> ha h b = g (h b) h' :: (Show ha) => t -> ha h' b = g ((h' b)::ha) Martin
Martin SULZMANN wrote:
Here's a simplified version.
h :: (Show ha) => t -> ha h b = g (h b)
g:: (Show ga) => ga -> gb g = undefined
In an attempt to discover the type signature of h, let us lift it:
g:: (Show ga,Show gb) => ga -> gb g = undefined
class (Show ha) => H t ha where h:: t->ha h b = g (h b)
gives us an error: Could not deduce (H t ha1) from the context (H t ha) Probable fix: Add (H t ha1) to the class or instance method `h' arising from use of `h' at /tmp/e.hs:10 In the first argument of `g', namely `(h b)' In the definition of `h': g (h b) However, if we change the class H into
class (Show ha) => H t ha | t->ha where h:: t->ha h b = g (h b)
everything typechecks. It seems very hard for me to avoid the thought that the type of the original h should be forall t ha. (Show ha) => t -> ha | t -> ha or, to re-write it into valid Haskell, forall t ha. (H t ha) => t -> ha That might answer my previous question... Regarding your observation:
g:: (Show ga) => ga -> gb g = undefined h :: (Show ha) => t -> ha h b = g (h b)
Same problem occurs. Though this is strange.
Consider type inference for
h b = g (h b)
We generate the following constraints:
th = tb -> ga, Show ga -- results from g (h b) th = tb -> gb -- taking into account h b = g (h b)
In case of
h :: (Show ha) => t -> ha h b = g (h b)
we additionally generate
th = t -> ha, Show ha
Overall, we find
th = tb -> ga, Show ga th = tb -> gb, th = t -> ha, Show ha
as my above calculation shows there shouldn't be a problem in the first place.
I think I can see the problem: if we have a function foo:: t1 -> t2 then GHC definitely knows that foo relates t1 and t2 by a functional dependency -- indeed, foo is a function. However, when presented with a type signature bar:: (C t3) => t3 -> t4 the compiler doesn't know if bar is a regular function, or if it is a method in the class C. In either case, the signature is just the same. If bar is a bona fide function, then t3 and t4 are related by a functional dependency. If bar is a method of C, things are not so clear. Well, they are clear for the single-parameter class C without overlapping instances (which GHC actually allows). However, for baz:: (D t5 t6 t7) => t6 -> t8 there could conceivably be instances of baz which relate the same t6 to two different t8. That's why we have to explicitly specify the functional dependency. I guess this might probably answer the original question Levent Erkok posed three years ago.
participants (3)
-
Keith Wansbrough -
Martin SULZMANN -
oleg＠pobox.com