# Can an entity has more than one type?

I think that 1 is natural number and real number, so $1:\mathbb{N}$ and $1:\mathbb{R}$.

In type theory, can an entity has more than one type?

• – JMoravitz Sep 17 '18 at 16:04

If you interpret "entity" as term, then the answer is "yes" for some type theories, namely ones that have some form of subtyping (which is sometimes implicit), and "no" otherwise. For example, the type theory implemented by NuPRL has subtyping and there are many terms which have multiple types e.g. $2$ has type $\mathbb Z$ and $\mathbb Z/5\mathbb Z$. On the other hand, the (core) type theory implemented by Coq doesn't have any subtyping (even implicitly, I believe) and so every term is in exactly one type. Most popular type theories do not have an explicit notion of subtyping, though fairly often there's an implicit subtyping relation between $\forall \alpha.T(\alpha)$ and its instances, e.g., $T(\mathbb Z)$.
• Type systems with intersection types are quite widely studied (Google it). Type systems of this kind will let you ascribe the type $\Bbb{N} \cap \Bbb{R}$ to $1$ and use it wherever a value of type $\Bbb{N}$ or $\Bbb{R}$ is required. – Rob Arthan Sep 17 '18 at 19:35
• @RobArthan I'm familiar with them. I would consider those forms of subtyping, i.e. $\mathbb N\cap\mathbb R \mathtt{<:}\mathbb N$ (and similarly for $\mathbb R$), but that is another good example. NuPRL also supports intersection types. (NuPRL is an odd duck in this space in many ways, though.) – Derek Elkins Sep 17 '18 at 19:44