Search code examples
haskelltypesfunction-definition

Finding the type of a composition function in Haskell

Let's say I have the following function in Haskell:

compose2 = (.) . (.)

How would I go about finding the type of this function? Because of the multiple compositions I get stuck trying to determine what the type of this function would be.

I know I can use :t compose2 to get the type. However, I want to know how to do it without the aid of a computer. What steps should I take to find the type?

Solution

  • It might help if we fist give the composition functions a more unique identifier, for example:

    compose2 = (.)₂ .₁ (.)₃

    that way it is easier to refer to some function. We can also convert this to a more canonical form, like:

    compose2 = ((.)₁ (.)₂) (.)₃

    so now we can start deriving the function type. We know that (.) has type (.) :: (b -> c) -> (a -> b) -> a -> c, or more canonical (.) :: (b -> c) -> ((a -> b) -> (a -> c)). Since the type variables are not "global", we thus can give the tree functions different names for the type variables:

    (.)₁ :: (b -> c) -> ((a -> b) -> (a -> c))
(.)₂ :: (e -> f) -> ((d -> e) -> (d -> f))
(.)₃ :: (h -> i) -> ((g -> h) -> (g -> i))

    so now that we have given the different composition functions a signature, we can start deriving the types.

    We know that (.)₂ is the parameter of a function application with (.)₁, so that means that the type of the parameter (b -> c) is the same as the type (e -> f) -> ((d -> e) -> (d -> f)), and therefore that b ~ (e -> f), and c ~ ((d -> e) -> (d -> f)).

    We furthermore know that the type of the "second" parameter of (.)₁ is the same as the type of (.)₃, so (a -> b) ~ ((h -> i) -> ((g -> h) -> (g -> i))), and therefore a ~ (h -> i), and b ~ ((g -> h) -> (g -> i)), therefore the "return type" of (.)₁, which is (a -> c) can thus be specialized to:

    ((.)₁ (.)₂) (.)₃ :: a -> c

    and since a ~ (h -> i), and c ~ (d -> e) -> (d -> f):

    ((.)₁ (.)₂) (.)₃ :: (h -> i) -> ((d -> e) -> (d -> f))

    we know that b is equivalent to both b ~ (e -> f) and b ~ ((g -> h) -> (g -> i)), so that means that e ~ (g -> h), and f ~ (g -> i), we thus can specialize the signature further to:

    ((.)₁ (.)₂) (.)₃ :: (h -> i) -> ((d -> (g -> h)) -> (d -> (g -> i)))

    which is a more verbose form of:

    (.)₂ .₁ (.)₃ :: (h -> i) -> (d -> g -> h) -> d -> g -> i

    If we automatically derive the type, we obtain:

    Prelude> :t (.) . (.)
(.) . (.) :: (b -> c) -> (a1 -> a -> b) -> a1 -> a -> c

    If we thus replace b with h, c with i, a1 with d and a with g, we obtain the same type.