CODEWITHSUNDEEP
typesocaml
user3011240
user3011240

Reputation: 97

Why does this OCaml expression have the following type?

The expression is f x y = 1 + (x 1) + (y 1) which has a type of (int->int)->(int->int)->int. I don't understand how it has that type. why isn't it int->int?

Upvotes: 1

Views: 100

Answers (4)

Jackson Tale
Jackson Tale

Reputation: 25812

let f x y = 1 + (x 1) + (y 1)

  1. you have (x 1), so x must be a function

  2. you have 1 + (x 1), so (x 1) must return an int, also 1 is int, so x: int -> int <fun>

  3. using the same induction as above, y: int -> int <fun>

  4. you have f x y, so f is a function, we already know what type x and y is and also know the right handside of = must be an int, so f: (int -> int) -> (int -> int) -> int

Upvotes: 2

ivg
ivg

Reputation: 35210

When OCaml infers the type of expression

let f x y = 1 + (x 1) + (y 1)

It will think something like this:

  1. Since (+) has type int -> int, expression (x 1) should have type int, as it occurs on the right hand side of +.

  2. Since x 1 should evaluate to int and it is an application, it should have type _ -> int. As 1 is an int literal, it has type int -> int.

  3. Using the same logic we can infer, that y also has type int -> int.

Upvotes: 3

Syed Jafri
Syed Jafri

Reputation: 194

Since you have function applications (x 1) and (y 1). x and y are treated like functions that take an int argument and return an int.

So x is type (int -> int) and y is type (int -> int). 1 is applied on both x and y. So if 1 is applied on something that is type (int -> int) you get something that is type int. So your whole function returns 1 + int + int which is basically int.

Upvotes: 3

Jeffrey Scofield
Jeffrey Scofield

Reputation: 66793

The expression (x 1) requires x to be a function of type int -> 'a. Similarly for (y 1). The rest follows from this.

Upvotes: 2

Related Questions