# Function Definitions

The following code

```
let x = 42
```

has an expression in it (`42`

)
but is not itself an expression. Rather, it is a *definition*.
Definitions bind values to names, in this case the value `42`

being
bound to the name `x`

. The OCaml manual has definition of
all definitions
(see the third major grouping titled "*definition*" on that page), but again
that manual page is primarily for reference not for study.
Definitions are not expressions, nor are expressions definitions—
they are distinct syntactic classes. But definitions can have expressions
nested inside them, and vice-versa.

For now, let's focus on one particular kind of definition, a *function definition*.
Non-recursive functions are defined like this:

```
let f x = ...
```

Recursive functions are defined like this:

```
let rec f x = ...
```

The difference is just the `rec`

keyword. It's probably a bit surprising that
you explicitly have to add a keyword to make a function recursive, because
most languages assume by default that they are. OCaml doesn't make that
assumption, though.

One of the best known recursive functions is the factorial function. In OCaml it can be written as follows:

```
(* requires: n >= 0 *)
(* returns: n! *)
let rec fact n =
if n=0 then 1 else n * fact (n-1)
```

We provided a specification comment above the function to document the
precondition (`requires`

) and postcondition (`returns`

) of the function.

Note that, as in many languages, OCaml integers are not the "mathematical" integers but are limited to a fixed number of bits. The manual specifies that integers are at least 30 bits but might be wider. So if you test on large enough inputs, you might begin to see strange results. The problem is machine arithmetic, not OCaml.

Here's another recursive function:

```
(* requires: y>=0 *)
(* returns: x to the power of y *)
let rec pow x y =
if y=0 then 1
else x * pow x (y-1)
```

Note how we didn't have to write any types in either of our functions:
the OCaml compiler infers them for us automatically. The compiler
solves this *type inference* problem algorithmically, but we could do
it ourselves, too. It's like a mystery that can be solved by our
mental power of deduction:

Since the if expression can return

`1`

in the`then`

branch, we know by the typing rule for`if`

that the entire if expression has type`int`

.Since the if expression has type

`int`

, the function's return type must be`int`

.Since

`y`

is compared to`0`

with the equality operator,`y`

must be an`int`

.Since

`x`

is multiplied with another expression using the`*`

operator,`x`

must be an`int`

.

If we did want to write down the types for some reason, we could do that:

```
(* requires: y>=0 *)
(* returns: x to the power of y *)
let rec pow (x:int) (y:int) : int =
if y=0 then 1
else x * pow x (y-1)
```

When we write the *type annotations* for `x`

and `y`

the parentheses are
mandatory. We will generally leave out these annotations, because
it's simpler to let the compiler infer them. There are other times when you'll
want to explicitly write down types though. One particularly useful time
is when you get a type error from the compiler that doesn't make sense.
Explicitly annotating the types can help with debugging such an error message.

**Syntax.**
The syntax for function definitions:

```
let rec f x1 x2 ... xn = e
```

The `f`

is a metavariable indicating an identifier being used as a function
name. These identifiers must begin with a lowercase letter. The remaining
rules for lowercase identifiers can be found in the manual.
The names `x1`

through `xn`

are metavariables indicating argument identifiers.
These follow the same rules as function identifiers. The keyword `rec`

is required if `f`

is to be a recursive function; otherwise it may be omitted.

Note that syntax for function definitions is actually simplified compared to what OCaml really allows. We will learn more about some augmented syntax for function definition in the next couple weeks. But for now, this simplified version will help us focus.

Mutually recursive functions can be defined with the `and`

keyword:

```
let rec f x1 ... xn = e1
and g y1 ... yn = e2
```

For example:

```
(* [even n] is whether [n] is even.
* requires: [n >= 0] *)
let rec even n =
n=0 || odd (n-1)
(* [odd n] is whether [n] is odd.
* requires: [n >= 0] *)
and odd n =
n<>0 && even (n-1);;
```

The syntax for function types:

```
t -> u
t1 -> t2 -> u
t1 -> ... -> tn -> u
```

The `t`

and `u`

are metavariables indicating types. Type `t -> u`

is the
type of a function that takes an input of type `t`

and returns an output
of type `u`

. We can think of `t1 -> t2 -> u`

as the type of a function
that takes two inputs, the first of type `t1`

and the second of type
`t2`

, and returns an output of type `u`

. Likewise for a function that
takes `n`

arguments.

**Dynamic semantics.**
There is no dynamic semantics of function definitions. There is nothing
to be evaluated. OCaml just records that the name `f`

is bound to a function
with the given arguments `x1..xn`

and the given body `e`

. Only later, when
the function is applied, will there be some evaluation to do.

**Static semantics.**
The static semantics of function definitions:

- For non-recursive functions: if by assuming that
`x1:t1`

and`x2:t2`

and ... and`xn:tn`

, we can conclude that`e:u`

, then`f : t1 -> t2 -> ... -> tn -> u`

. - For recursive functions: if by assuming that
`x1:t1`

and`x2:t2`

and ... and`xn:tn`

and`f : t1 -> t2 -> ... -> tn -> u`

, we can conclude that`e:u`

, then`f : t1 -> t2 -> ... -> tn -> u`

.

Note how the type checking rule for recursive functions assumes that the
function identifier `f`

has a particular type, then checks to see whether
the body of the function is well-typed under that assumption. This is
because `f`

is in scope inside the function body itself (just like the arguments
are in scope).