A function is an input-output relation, that is, we can think of a function as a machine, or process, that takes inputs and produces outputs according to some rule(s). For each element of the domain, or input type, a function specifies a single element of the codomain, or output type.
The type of a function with domain
B is written
A -> B (or
A → B).
Two simple examples of functions are shown below.
f : N -> N f(n) = 3n + 1 g : N * N -> Q g(x,y) = f(x) / (y - 1)
f takes natural numbers as input and
produces natural numbers as output; for a given input
produces the output
3n + 1.
g takes pairs of natural
numbers as input, and produces rational numbers;
given the pair
(x,y), it produces
f(x) / (y - 1) as output.
Functions can be given names and defined by pattern-matching, as in the examples above.
Functions can also be defined anonymously, using lambda notation. For example,
\n. 3n + 1
is the function which takes an input called
3n + 1. This is the same function as the example function
Attempting to print a function value will simply result in the type of the function being printed as a placeholder:
Disco> (\n. 3n+1) <ℕ → ℕ>
This is because once a program is running, Disco has no way in general to recover the textual definition of a function.