Function with respect to Programming language
A function is a unit of code that is often defined within a greater code structure. Specifically, a function contains a set of code that works on many kinds of inputs, like variants, expressions and produces a concrete output.
Let us consider the example a:= (24). a:= (24) has an expression in it but (24) is not itself an expression. Rather, it is a function definition. Definitions bind values to names, in this case the value 24 being bound to the name ‘a’. Definitions are not expressions, at the same time expressions are also not treated as definitions. Definitions are distinct syntactic blocks. Definitions can have expressions nested inside them, and vice-versa.
Parameters are the variables in a function definition and arguments are the values which are passed to a function definition.
Let us see an example of a function definition:
(requires: b>=0 )
(returns: a to the power of b)
let rec pow a b:=
if b=0 then 1
else a * pow a (b-1)
In the above function definition variable ‘b’ is the parameter and the value which is passed to the variable ‘b’ is the argument. The precondition (requires) and postcondition (returns) of the function is given. Note we have not mentioned any types: (data types). Some language compiler solves this type (data type) inference problem algorithmically, but some require the type to be mentioned.
In the above function definition if expression can return 1 in the then branch, by the typing rule the entire if expression has type int. Since the if expression has type ‘int’, the function's return type also be ‘int’. ‘b’ is compared to 0 with the equality operator, so ‘b’ is also a type of ‘int’. Since ‘a’ is multiplied with another expression using the * operator, ‘a’ must be an int.
Now let us write the same function definition with types for some reason:
(requires: b> 0 )
(returns: a to the power of b )
let rec pow (a: int) (b: int) : int := if b=0 then 1
else a * pow b (a-1)
When we write the type annotations for ‘a’ and ‘b’ the parentheses are mandatory. Generally we can leave out these annotations, because it's simpler to let the compiler infer them. There are times we may want to explicitly write down types. This is useful on times 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.
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”.
Syntax: The syntax for function definitions:
let rec fna1 a2 ... an := k
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.
For example: let us see an example to check whether the entered number is even or odd.
(requires: x>= 0)
let rec even x :=
x=0 || odd (x-1)
(requires: x>= 0)
let odd x :=
x<>0 && even (x-1)
The syntax for function types:
x → y
x1 → x2 → y
x1 → ... → xn → 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.