A function like $f(x) = 2x$ can be defined over the reals so its “type signature” or in set theory domain and codomain is $f: \mathbb{R} \rightarrow \mathbb{R}$.
I want to define a function $f(x) = 5$ (or some other constant number) and restrict the codomain/return type to be a constant value. What is the (most restrictive) type signature of such a function? Does this require dependent types? Is it $f: \mathbb{R} \rightarrow 5$? I want to know the type signature for that specific function that returns $5$ and the more general notion of a function that returns a constant value that does not depend on the input argument.
My motivation is that I want to be able to describe in a precise way functions that do not use/“delete” their input argument and return some other constant value. Eventually, I want to formalize this in a proof assistant.
Best Answer
The answer to this really depends on your type theory. The type theories of proof assistants like Coq or Agda will let you express any of the following classes as types:
$$ \{f : \Bbb{R} \to \Bbb{R} \mid \forall x:\Bbb{R}\cdot f(x) = 5\} \\ \{f : \Bbb{R} \to \Bbb{R} \mid \exists c:\Bbb{R}\cdot \forall x:\Bbb{R}\cdot f(x) = c\} \\ \bigcup_Y \{f : \Bbb{R} \to Y \mid \exists c:Y\cdot \forall x:\Bbb{R}\cdot f(x) = c\} \\ \bigcup_{X, Y} \{f : X \to Y \mid \exists c:Y\cdot \forall x:X\cdot f(x) = c\} $$ and many variations on this kind of theme. Weaker type theories might not be able to deal with some of the above.