Warm tip: This article is reproduced from serverfault.com, please click

Finding the type of a composition function in Haskell

发布于 2020-11-28 14:10:15

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?

Questioner
Miles Cox
Viewed
0
Willem Van Onsem 2020-11-28 22:27:03

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

compose2 = (.)2 .1 (.)3

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

compose2 = ((.)1 (.)2) (.)3

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:

(.)1 :: (b -> c) -> ((a -> b) -> (a -> c))
(.)2 :: (e -> f) -> ((d -> e) -> (d -> f))
(.)3 :: (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 (.)2 is the parameter of a function application with (.)1, 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 furtermore know that the type of the "second" parameter of (.)1 is the same as the type of (.)3, 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 (.)1, which is (a -> c) can thus be specialized to:

((.)1 (.)2) (.)3 :: a -> c

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

((.)1 (.)2) (.)3 :: (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:

((.)1 (.)2) (.)3 :: (h -> i) -> ((d -> (g -> h)) -> (d -> (g -> i)))

which is a more verbose form of:

(.)2 .1 (.)3 :: (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.