07 Function Types

Let's take a closer look at the static semantics, or type checking, of functions.

Type t -> u is the type of a function that takes in input of type t and returns an output of type u.

Type t1 -> t2 -> u is the type of a function that takes an input of type t1 and another input of type t2, and returns an output of type u. The last type (at the end of all of the arrows) is always the output of the function.

Notice that there's a dual purpose for the -> syntax. It's being used for the function types, and function values when using the keyword fun. That's nice because they're both pretty similar!

The type checking rules state:

• If x1 : t1, ..., xn : tn
• and e : u
• then (fun x1 ... xn -> e) : t1 -> ... -> tn -> u

Let's look at some examples!

fun (x : int) -> x + 1;; (* OCaml doesn't need us to explicitly declare this type, but we do it for the sake of the demo*)

- : int -> int = <fun>

We can see that x + 1 has a type int, and x has a type int, so the function has a type int -> int.

What about multiple inputs?

fun x y -> x + y;;

- : int -> int -> int = <fun>

OCaml implicitly determines the types:

• x : int
• y : int

Since x and y are ints, we can see that x + y is an int, so the function has type int -> int -> int.

Function application has very similar rules:

• If e0 : t1 -> ... -> tn -> u and e1 : t1, ..., en : tn
• Then e0 e1 ... en : u.