The syntax for function types:
\({ }^{*} \mathrm{x} \rightarrow \mathrm{y} \quad{ }^{*} \mathrm{xl} \rightarrow \mathrm{x} 2 \rightarrow \mathrm{y} \quad{ }^{*} \mathrm{xl} \rightarrow \ldots \rightarrow \mathrm{xn} \rightarrow \mathrm{y}\)
The 'x' and 'y' are variables indicating types. The type x → y is the type of a function that gets an input of type 'x' and returns an output of type 'y'. Whereas x1 → x2 → y is a type of a function that takes two inputs, the first input is of type 'x1' and the second input of type 'x2', and returns an output of type 'y'.
Likewise x1 → ... → xn → y has type 'x' as input of n arguments and 'y' type as output.

let minxyz:=
if x <y then x else z;
else
if y< 2 then y else z;

Program:
(requires:x > = 0)
let rec even x: = 
x= 0||odd (x-1)
return 'even'
(requires: x> = 0)
let odd x: =
x<>&&even (x-1)
return 'odd'

The mathematical function random () will give different outputs for the same function call.
let Random number
let a:= random()
if a>10 then return: a
else return: 10
Here the function Random is impure as it is not sure what will be the result when we call the function.

There are various theoretical advantages of having pure functions. one advantage is that if a function is pure, then if it is called several times with the same arguments, the compiler only needs to actually call the function once.
Let see an example
let i:=0;
if i<strlen(s) then
--Do something which doesn't affects
++i
If the compiler is smart to enough to work out that strlen is a pure function and that 's' is not updated in the loop, then it can remove the redundant extra calls to strlen and make the loop to execute only one time.

Pure functions are functions which will give exact result when the same arguments are passed. A function can be a pure function provided it should not have any external variable which will alter the behaviour of that variable.
Example:
let square x
return: x*x
The above function square is a pure function because it will not give different results for same input.

The syntax for function types
x\(\rightarrow \)y
x1 \(\rightarrow \)x2\(\rightarrow \)y
x1 \(\rightarrow \) .... \(\rightarrow \)x n\(\rightarrow \)y
The 'x' and 'y' are variables indicating types. The type x \(\rightarrow \) y is the type of a function that gets an input of type 'x' and returns an output of type 'y'. Where as x1\(\rightarrow \) x2 -\(\rightarrow \) y is a type of a function that takes two inputs, the first input is of type 'x1' and the second input of type 'x1', and returns an output of type 'y'. Likewise x1 \(\rightarrow \)...\(\rightarrow \)x n\(\rightarrow \)y has type 'x' as input of n arguments and 'y' type as output.

(requires: x>= 0)
let rec even x :=
x=0II odd (x-I)
return 'even'
(requires: x > = 0)
let odd x :=
x< >0 && even (x-I)
return 'odd'

(i) The syntax to define functions is close to the mathematical usage: the definition is introduced by the keyword let, followed by the name of the function and its arguments; then the formula that computes the image of the argument is written after an = sign. If you want to define a recursive function: use "let rec" instead of "let".
(ii) Syntax: The syntax for function definitions:
let rec fn a1 a2 ... an :;= k
(iii) Here the 'fn' is a variable indicating an identifier being used as a function name. The names 'a1' to 'an' are variables indicating the identifiers used as parameters. The keyword 'rec' is required if 'fn' is to be a recursive function; otherwise it may be omitted.