Lecture 2.1: Functions

Last time, we started to covered the basics of OCaml; Today we will learn all about functions.

Editing OCaml in VSCode

Let's create tst.ml in VSCode, and fill it with the following contents:

tst.ml

let x = 3

let y = x + 1

let _ = 
    (* Print the value of y *)
    print_endline ("Value of y: " ^ string_of_int y)

(Ignore the last three lines for now; we will revisit this next class.) Note that the ;; separator is not required in ml files. Also, see that comments are written in OCaml like (* ... *).

Now, hover over various variables to see their types. You should see, for example, that x has type int, while "Value of y: " has type string. If you hover over +, you will see it has type int -> int -> int; this is the type of a function that takes two integers and returns an integer. You will also see some helpful documentation. Similarly, if you hover over string_of_int, you will see it has type int -> string.

To run it, we have a few options:

Use ocamlc to compile it:
```
ocamlc tst.ml -o tst
./tst
```
Interpret it using utop:
```
utop tst.ml
```

Load it using utop, which will make the bindings available in the REPL:

utop # #use "tst.ml";;
val x : int = 3
val y : int = 4
Value of y: 4
- : unit = ()

utop # x + y;;
- : int = 7

Functions

So far, we have seen the basic OCaml types int, bool, and string. Now, let's look at functions. OCaml, being a functional programming language, makes functions very easy to use and manipulate. To create a function, we can use the syntax fun (x : t) -> e, where t is a type and e is an expression:

utop # fun (x : int) -> x + 1;;
- : int -> int = <fun>

Type annotations

We will see later in the class that type annotations can be optional. For now, we will use them throughout.

The value fun (x : int) -> x + 1 is an OCaml value, just as 3 or "hi" is. However, unlike int or string, we get a function type, written t1 -> t2, where t1 and t2 are types. The <fun> syntax is OCaml's way of printing the value of the function.

Functions can be applied to arguments by writing them next to each other (and inserting parentheses where needed):

utop # (fun (x : int) -> x + 1) 3;;
- : t = 4

Note that we needed to wrap the fuction in parentheses; if we didn't, we would get a type error:

utop # fun (x : int) -> x + 1 3;;
Error: This expression has type int
       This is not a function; it cannot be applied.

This is because OCaml would parse this as fun x : int -> x + (1 3), and this would mean treating 1 as a function and applying it to the argument 3.

Because functions are values, we can manipulate them just like other values, including let-binding them:

utop # let f = fun (x : int) -> x + 1;;
val f : int -> int = <fun>

utop # f 2;;
- : int = 3

utop # let my_fun = 
        let f = fun (x : int) -> x + 1  in   
        let g = fun (y : int) -> f y + 1 in 
        fun (z : int) -> g (g z);;
val my_fun : int -> int = <fun>

utop # my_fun 2;;
- : int = 6

Multi-argument functions

Because functions are not special in OCaml relative to other types (e.g., integers or strings), they can return other functions:

utop # let f = fun (x : int) -> fun (y : int) -> x + y;;
val f : int -> int -> int = <fun>

Here, f has type int -> int -> int. This should be read as int -> (int -> int) (i.e., -> is right associative); in other words, f is a function which, given an int, returns a function of type int -> int.

Instead of thinking of f as a function which returns a function, we can also think of it as a function which takes two arguments. Indeed, f's declaration can be abbreviated as follows:

utop # let f = fun (x : int) (y : int) -> x + y;;
val f : int -> int -> int = <fun>

Additionally, an alternative (often more convenient) syntax for writing functions is as follows:

utop # let f (x : int) = x + 1;;
val f : int -> int = <fun>

All three of the above declarations for f are equivalent.

This style of writing functions also works with multiple arguments:

utop # let f (x : int) (y : int) = x + y;;
val f : int -> int -> int = <fun>

Annotating return types

When you write functions like this, you can annotate the return type:

utop # let f (x : int) (y : int) : int = x + y;;
val f : int -> int -> int = <fun>

You can do this with regular values, too:

utop # let x : int = 3;;
val x : int = 3

Partial Application

Since multi-argument functions in OCaml are just functions which return functions, we can partially apply them:

utop # let f (x : int) (y : int) = x + y;;
val f : int -> int -> int = <fun>

utop # let add_two = f 2;;
val add_two : int -> int = <fun>

utop # add_two 8 ;;
val - : int = 10

Higher-order functions

Functions can also be higher-order, meaning they can take functions as inputs (because function types are treated the same as any other type):

utop # let f (g : int -> int) = g 2;;
val f : (int -> int) -> int = <fun>

utop # f (fun (x : int) -> x * 5);;
- : int = 10

Note that f's type is (int -> int) -> int; this is a single argument function that takes a function of type int -> int as its argument. This is different than int -> int -> int, which takes two arguments of type int.

Exercise

What will this evaluate to?

utop # let f (g : int -> int) (x : int) = g (x + 1);;
val f : (int -> int) -> int -> int = <fun>

utop # f (fun x -> x * 5) 3;;
_ : int = ???

Exercise

What will this evaluate to?

utop # let f (g : (int -> int) -> int) (x : int) = g (fun y -> x + y);;
val f : ((int -> int) -> int) -> int -> int = <fun>

utop # f (fun h -> h 42) 10;;
- : int = ???

Specifying a "maximum" function

Already with the ingredients that we have --- namely, higher-order functions --- we can already start to study what it means to write a specification. We will do so with a case study, a three-valued version of max:

(* Return the highest of the three inputs. *)
let max3 (i : int) (j : int) (k : int) = ...

How do we know we got it right?

The specification in the comment is pretty unambiguous. But given this implementation..

let max3 (i : int) (j : int) (k : int) = 
    if i >= j then 
        if i >= k then 
            i
        else 
            k
    else 
        if j >= k then 
            j
        else k

how do we know it is right? We could manually inspect it, but that won't work all the time (think about max4!), and is really easy to get wrong.

Instead, we want to implement the comment specification as a piece of formal logic, implemented in OCaml. How would we do so?
First, before trying to implement it, let's write down the mathematical property max3 should have.

\(\forall i, \forall j, \forall k, \mathsf{max3}(i, j, k) >= i \wedge \mathsf{max3}(i, j, k) >= j \wedge\mathsf{max3}(i, j, k) >= k.\)

Is this correct? Is this sufficient? In other words, we are looking for a formula that encodes our intuition. If there is a solution for \(\mathsf{max3}\) that is different than what we actually want, that means there's a problem with the formula. I claim there are functions that make the above formula true, but you wouldn't count as a valid version.

Here's a fixed version: \(\forall i, \forall j, \forall k, \mathsf{max3}(i, j, k) >= i \wedge \mathsf{max3}(i, j, k) >= j \wedge\mathsf{max3}(i, j, k) >= k \wedge \mathsf{max3}(i, j, k) \in \{i,j,k\}.\)

Next, we can implement the property. How could we turn this into a piece of OCaml code?

let max3_spec (f : int -> int -> int -> int) (i : int) (j : int) (k : int) : bool = 
    let z = f i j k in 
    z >= i && z >= j && z >= k && (z == i || z == j || z == k)