0
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

It depends on what you mean by "entity" and which type theory you are considering.

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)$.

On the other hand, if you interpreted "entity" as an element of the interpretation of a type for a given a (set-theoretic) semantics, say, then there's nothing (in general) that stops the interpretations of different types from overlapping or even being identical. That said, in my experience, type theorists either don't consider semantics or they tend to use categorical semantics. For categorical semantics, terms of different types will almost certainly be arrows between different objects and quite possibly in different categories. Whether such arrows are comparable depends on the meta-logic in which you formulated your notion of "category". For ZFC or most common set theories, they would be, but most categorists would consider these questions that are meaningless. As such, there are some meta-logics (such as FOLDS) and formulations of categories in those meta-logics where such questions are simply not askable, i.e. equality of arrows in different hom-sets is simply never a well-formed formula.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Rob Arthan Sep 17 '18 at 19:35
  • $\begingroup$ @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.) $\endgroup$ – Derek Elkins Sep 17 '18 at 19:44
  • $\begingroup$ Derek: sure. I knew you'd know about intersection types. I thought they might be of interest to the OP. Cheers! $\endgroup$ – Rob Arthan Sep 17 '18 at 19:47

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.