haskellpointfree

What is the resulting type of a simple pointfree implentation of dot product in Haskell?


In Haskell, if you convert a standard dot product of two lists such as

dotProduct :: (Num a) => [a] -> [a] -> a
dotProduct x y = sum $ zipWith (*) x y

through a pointfree tool like pointfree.io it produces

dotProduct = (sum .) . zipWith (*)

If I work through unifying the types I'm sufficiently convinced that the resulting type is indeed [a] -> [a] -> a along with the requisite typeclasses. Instead I'm confused why my first attempt

dotProduct = sum . zipWith (*)

fails in such a strange way. I would understand some kind of type error but it indeed type checks and on ghci its resulting type is (Foldable ((->) [c]), Num c, Num [c]) => [c] -> [c] which I can't even begin to understand. Is there an example inhabitant of this type that I could pass into the dot product?

When I try to run the type unification algorithm in manually it seems the first argument of sum [a] should unify with the ending part [c] -> [c] of zipWith (*). I think this should give a type error but instead it somehow unifies and that's what leads to the strange function.


Solution

  • When I try to run the type unification algorithm in manually it seems the first argument of sum [a] should unify with the ending part [c] -> [c] of zipWith (*).

    Mostly correct, but sum can take any foldable type, not only lists.

    I think this should give a type error but instead it somehow unifies and that's what leads to the strange function.

    sum takes any t a as long as t is a foldable, and a is a numeric type. In this case we have

    t a = [c] -> [c]
    -- i.e., rewriting the function type in prefix notation
    t a = (->) [c] [c]
    -- ergo
    t = (->) [c]
    a = [c]
    

    So this generates the requirements Foldable ((->) [c]) and Num [c].

    Sure, such constraints are not satisfied by the standard instances in play. Still, Haskell allows one to add their own instances. Doing so would likely involve writing weird, contrived instances, but it's theoretically possible and GHC would be wrong to reject this at this time.

    As a contrived example, take c = Void, the empty type with no (non bottom) values. If we ignore bottoms, then [c] is [Void] which only has one value (the empty list []), so [c] is isomorphic to the unit type ().

    Up to isomorphism, the constraints Foldable ((->) [c]) and Num [c] become Foldable Identity and Num (). The former instance already exists. The latter could be defined making () correspond to zero. A kind of zero-bits integer, so to speak.

    (Finally, we also need to satisfy the other constraint generated by zipWith(*), i.e. Num Void. This can not be done in a sensible way, as far as I can see. Still, GHC can not easily detect that.)