On maandag, sep 22, 2003, at 00:07 Europe/Amsterdam, Brandon Michael Moore wrote:
Can anyone tell me what's wrong with the following derivation?
Without going through your derivation completely, the problem is almost certainly polymorphic recursion. Vector is a nested datatype---its definition calls itself with different type arguments---and so, although collect :: (v -> [a]) -> (w -> [a]) -> Vector v w -> [a] the recursive call to collect in, for example, the second clause, has a different type, namely: collect :: (v -> [a]) -> ((w,w) -> [a]) -> Vector v w -> [a] However, in the absence of an explicit type signature, Haskell will assume that the types of the top-level and recursive occurrences of collect are equal, which they are not, so you'll get a type error. Indeed, the error messages Dominic posted:
ERROR "Test1.hs":23 - Type error in function binding *** Term : coal_ *** Type : (a -> b) -> (c -> [d]) -> Vector_ a e -> b *** Does not match : (a -> b) -> ((c,c) -> [d]) -> Vector_ a (e,e) -> b *** Because : unification would give infinite type
Test1.hs:25: Occurs check: cannot construct the infinite type: t = (t, t1) Expected type: (t, t1) Inferred type: t In the first argument of `coalw', namely `w1' In the first argument of `(++)', namely `(coalw w1)'
corroborate this argument. Or, are you asking instead why it is that type inference does not work for polymorphic-recursive functions? Regards, Frank