1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ $f$ goes from a set into a set, so write $f:\mathbb{R}\to\{5\}$ $\endgroup$ – user376343 Nov 27 '18 at 20:21
  • $\begingroup$ Since the actual value of 5 seems not to matter, why not $f : \mathbb{R} \to \{\ast\}$, where $\{\ast\}$ is a set containing a single element? $\endgroup$ – Xander Henderson Nov 27 '18 at 20:23
  • $\begingroup$ @XanderHenderson: your comment immediatley made me respond, that the OP is asking for the most restrictive type, but then I realised the question is unclear. $\endgroup$ – Rob Arthan Nov 27 '18 at 20:27
  • $\begingroup$ @RobArthan But they also seem, as per this comment, to be indicating that the actual value of the constant doesn't matter, hence my confusion. $\endgroup$ – Xander Henderson Nov 27 '18 at 20:31
  • $\begingroup$ @XanderHenderson: I agree: I edited my comment to point out the unclarity. $\endgroup$ – Rob Arthan Nov 27 '18 at 20:32
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

Define the type $\mathsf{Five}$ as the singleton type populated by the type axiom $E \vdash 5 : \mathsf{Five}$. Then the type of $f$ is $f : \mathbb{R} \rightarrow \mathsf{Five}$.

$\endgroup$
  • $\begingroup$ Thanks! What if I want a more general form that will cover any constant value from $\mathbb{R}$. Something like $f : \mathbb{R} \rightarrow c$ where $c$ is a constant value that does not depend on the input variable $x$. $\endgroup$ – Brandon Brown Nov 27 '18 at 20:22
  • $\begingroup$ You can define a singleton type $\mathsf{T}_x$ for any element $x$. $\endgroup$ – Hans Hüttel Nov 27 '18 at 20:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.