Do mathematical objects have underlying types? I came upon this issue while I was trying to think about what "type" of object is $\mathbb R^n$ - is it a set, a vector space, an inner product space, an affine space, a metric space? Perhaps the simplest way is to define $\mathbb R^n$ as simply being an object of type "set", and then construct new objects such as the vector space $\mathbb R^n$, which possesses an additional structure by having the operations of vector addition and scalar multiplication, or the metric space $\mathbb R^n$, which possesses the additional structure of a metric.
It seems often the case, at least in real analysis, however, that we wish to work with an object (denoted $\mathbb R^n$) which possesses both the algebraic structure afforded by being a vector space and the geometric structure afforded by being a metric space. While I can do all of the calculations, treating $\mathbb R^n$ as both a vector space and a metric space, I am troubled by the fact that I'm not sure which type of object I'm working with. Is it a metric space, or is it a vector space? Is it both? Neither? How should I think about this? (for both the "type" of $\mathbb R^n$ and for mathematical objects in general)
I added a few tags that I thought might be relevant (in areas I'm not quite familiar with), but mods should feel free to remove them if they're not appropiate.
 A: Putting things together into an answer and expanding significantly.
First, as T. Bongers stated, this is a form of notational overloading that is usually intended to be resolved by context.  The context may be either broad conventions ("standards") such as $\mathbb R^n$'s metric structure, canonical choices such as $\mathbb R$'s field structure, or the convention may be defined in the text you're reading.
Still, if we didn't want to rely on context what would we do and what does this overloading "resolve" to anyway?  The typical approach to be more explicit in informal (by which I mean "not machine checked") texts is to do the following:
$$\mathbb{R} \text{ is the set of real numbers} \\ (\mathbb{R},+,0) \text{ is the additive monoid of real numbers} \\ (\mathbb{R},\times,+,1,0) \text{ is the semiring of real numbers}$$
This clearly articulates the additional structure a monoid and a semiring have and what choices we are making here.  If we want to treat a semiring as a monoid, we'd have to explicitly forget the extra structure: $U_M(t,m,a,u,z) = (t,m,u)$ (note we'd also have $U_A(t,m,a,u,z) = (t,a,z)$, both $U_M, U_A : \mathbf{SemiRing} \to \mathbf{Monoid}$).  Similarly, $U : \mathbf{Monoid} \to \mathbf{Set}$ would be $U(t,m,u) = t$.  Compare this with typical statements like $U(\mathbb R) = \mathbb R$.
Being this explicit can often be clarifying and helpful.  For example, it's much easier to see and articulate the adjunction in $$\mathbf{Monoid}(FS, M) \cong \mathbf{Set}(S, UM)$$ than in $$\mathbf{Monoid}(FS, M) \cong \mathbf{Set}(S, M)$$  The former can easily be expressed with $F \dashv U$, the latter is awkward to write down without introducing $U$.  
The tuple notation can also be very handy. Sticking with the above adjunction, if you want to explicitly define the counit, using the normal, implicit notation leads to some awkwardness and difficulty.  In the typical notation you'd be asked to define a natural transformation: $\varepsilon_M : FUM \to M$ natural in $M$.  The elements of $FUM$ for a monoid $M$ are just lists of elements of $M$.  We need to collapse that list into a single element by multiplying them all together by the monoid operation. $\varepsilon_M(ms) = \text{fold}(?,?,ms)$ but what do we put for the question marks?  It should be the multiplication and unit of the monoid, but what are they?  The free monoid construction has certainly forgotten them.  Moving to the more explicit notation, we see: $\varepsilon_{(M,\oplus,e)}(ms) = \text{fold}(\oplus,e,ms)$.
However, even the approach above is suppressing some aspects.  For example, what's the difference between a monoid and a commutative monoid?  There is no additional structure, just an additional property of the existing structure.  Taking a cue from type theory, the additional evidence we need that a monoid is a commutative monoid is a proof that the operation is commutative.  Once we make that explicit, we should then make explicit the evidence that the operation is associative and unital.  It's extremely rare for mathematicians to treat proofs as mathematical objects, but this is exactly what modern type theories do.
The cost of all this explicitness, of course, is verbosity and bureaucratic distinctions that can clutter up what is trying to be demonstrated.
