You are looking for extrinsic types which were explained by John Reynolds in his paper on intrinsic and extrinsic semantics.
Briefly, there are two ways in which we can approach types for programs:
- Intrinsic: a program without a typing is meaningless, i.e., we consider programs together with their types.
- Extrinsic: a program without typing information is meaningful. We can assign one or many types to it to express that it has certain properties.
Statically typed functional languages such as ML and Haskell insist on intrinsic typing: they refuse to run a program unless they can determine that it has a type. Scheme is untyped, so it will run a program even if no type can be assigned to it, and any types that are assigned to Scheme programs are extrinsic (external) to Scheme.
Let us consider an example. In $\lambda$-calculus we may consider the identity function. There are many ways to write it, depending on a particular flavor of the calculus:
- untyped: $\lambda x . x$
- monomorphic: $(\lambda x : \mathsf{int} . x) : \mathsf{int} \to \mathsf{int}$
- polymorphic (System F): $(\Lambda A . \lambda x : A . x) : \forall A . A \to A$
- parametric polymorphism (ML): $(\lambda x . x) : \alpha \to \alpha$
Under the intrinsic view of types we would insist that $\lambda x . x$ by itself means nothing, and that typing information must be provided. Under the extrinsic view $\lambda x . x$ makes sense by itself, but can be assigned many different types – so long as we explain what it means "to assign a type". A simple way is to say that a type is the same thing as a subset $T \subseteq \Lambda_0$ of the set $\Lambda_0$ all closed terms in the untyped $\lambda$-calculus (a better definition would be that a type is a partial equivalence relation on the set of closed terms). Some types that come to mind are:
- the type of terms equal to a Church numeral $$C = \{t \in \Lambda_0 \mid \exists n : \mathbb{N} . f \equiv_{\beta\eta} \overline{n} \}$$ where $\overline{n}$ is the $n$-th Church numeral.
- given any $A \subseteq \Lambda_0$ and $B \subseteq \Lambda_0$, we can define the type of functions $$A \to B = \{ t \mid \forall u \in A . t u \in B\}$$.
- if $(A_i)_{i \in I}$ is a family of types, we can define their intersection type $\bigcap_{i \in I} A_i$.
Now it can be checked that $\lambda x . x$ has the following extrinsic types:
- $C$ because it equals $\overline{1}$,
- $C \to C$
- $A \to A$ for any $A \subseteq \Lambda_0$
- $\bigcap_{A \subseteq \Lambda_0} (A \to A)$
An example that John Reynold liked to give was this: given a real number $c \in \mathbb{R}$, what type does $\lambda x . \cos(c \cdot x)$ have? Under intrinsic semantics the type would presumably be $\mathbb{R} \to \mathbb{R}$ no matter what $c$ is. But under extrinsic semantics it always has the type $\mathbb{R} \to \mathbb{R}$ and also the extrinsic type $\mathbb{Z} \to \mathbb{Z}$ when $c = \pi/2$.
