6

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?

Miles Cox
  • 63
  • 3
  • closely related: https://stackoverflow.com/questions/34701011/how-to-manually-infer-the-type-of – Will Ness Nov 28 '20 at 14:32
  • for an answer to "how to go about deriving type of *a* function in general" see e.g. [this](https://stackoverflow.com/a/14558244/849891) or browse through e.g. [these](https://stackoverflow.com/search?q=user%3A849891+mechanically) – Will Ness Nov 28 '20 at 14:37
  • Thanks for the suggestions! I wasn't able to find a similar post myself. – Miles Cox Nov 28 '20 at 15:23

1 Answers1

8

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.

rampion
  • 87,131
  • 49
  • 199
  • 315
Willem Van Onsem
  • 443,496
  • 30
  • 428
  • 555