hyperbug
hyperbug

Reputation: 5

OCaml Input types

I am learning OCaml and so far I am having trouble to understand the concepts of types.

For example, if we have this following code:

# let func x = x;;
val func : 'a -> 'a = <fun>

From the official website, it tells me that 'a before the arrow is the unknown input type and 'a after the arrow is the output.

However, when I try to use function composition:

# let composition f x = f(x);;
val composition : ('a -> 'b) -> 'a -> 'b = <fun>

What ('a -> 'b) means? Is 'a related to f and 'b related to x?

Another function composition that made me even more confused is:

# let composition2 f x = f(f(x));;
val composition2 : ('a -> 'a) -> 'a -> 'a = <fun>

I don't really understand why we don't have the 'b in this case.

Thank you in advance!

Upvotes: 0

Views: 233

Answers (1)

ForceBru
ForceBru

Reputation: 44828

'a -> 'b is the type of a function that takes one argument of type 'a and returns a value of type 'b.

val composition : ('a -> 'b) -> 'a -> 'b means that composition is a function of two arguments:

  1. the first one is of type ('a -> 'b), so a function as above
  2. the second one is of type 'a

So, this function returns something of the same type as the return type of the first argument, 'b. Indeed, it takes a function and its argument and applies that function to the argument.


In the second case, you can work backwards from the inner call. Let's have a look at f(f(x))

  1. x is something of any type 'b. We have no idea what kind of type this is yet.
  2. Since we have f(x), f must be a function of type 'b -> 'c. It's 'b because we know it takes x as input, and x is of type 'b.
  3. Thus, the type of composition2 is ('b -> 'c) -> 'b
  4. Since we have f(f(x)), the type of f's argument must be the same as the type of its return value. So, 'b == 'c. Call that type 'a.
  5. Since x is of type 'b, which is the same as 'a, x must be of type 'a.
  6. Since f is of type 'b -> 'c, where 'b == 'a and 'c == 'a, f must be of type 'a -> 'a.
  7. Thus, the type of composition2 is ('a -> 'a) -> 'a

Upvotes: 2

Related Questions