Can maths functions "return" multiple different mathematical objects? In computer science, there are statically and dynamically typed languages, with statically typed languages generally being stricter about types of variables, function parameters, etc. To what extent can maths be considered "statically typed" (obviously this isn't the correct term but hopefully you understand what I'm asking) and how strict is it?
For example, do mathematical functions always have to return the same mathematical object (e.g. number, vector, etc.), or can the "type" (to use a computer science term) vary depending on the arguments it receives? I was wondering whether something like this makes any sense:
$$
    f(x)= 
\begin{cases}
    x + 2& \text{if } x > 1\\
    [1, 2, 3]              & \text{otherwise}
\end{cases}
$$ i.e. $f(x)$ can return a number or a vector.
 A: A function $f: A \to B$ maps elements of a domain set $A$ to elements of a domain set $B$.
As a set can be any collection of objects, it doesn't actually make sense to talk of objects being different "types".
Consider the $B = \{2, \pi, [1,3,7], fish, Sherlock\ Holmes, invisible\ green\ thoughts\}$.
$2$ is a natural number, $\pi$ is a transcendental irrational real number, $[1,3,7]$ is a vector, $fish$ is a group of animals, $Sherlock\ Holmes$ is a fictional character, $invisible\ green\ thoughts$ is a hypothetical idea of Noam Chomsky.  Are these the same type of object?
The answer is a emphatic:  YES!  The are all objects of the type-- Belonging to set $B$.
And $f: \mathbb N \to B$ via $$f(n) = \begin{cases} 2&\text{if }n\text{ is prime}\\\pi&\text{if }n\text{ is even composite}\\ [1,3,7]&\text{if }n\text{ is an odd perfect square}\\Sherlock\ Holmes&\text{otherwise}\end{cases}$$ is a perfectly valid (non-surjective) function that does what a good function should; it maps every element of a specific set ($\mathbb N$) to a distinct element of a specific set ($B$).
A: 
can the "type" (to use a computer science term) vary depending on the arguments it receives

That is typically what a dependent type theory allows, with dependent product types and many other constructions.
That does however not mean that a dependent type cannot be verified "statically": in a constructive type theory, type checking is usually decidable.
