Translating typed functional language to untyped lambda calculus Defining a typed function in haskell,

double::Integer-&gt;Integer
double a = a + a


And we can get an untyped version of double and let's call it double' to distinguish from the typed one.
Then, we can't prevent someone from passing a non-integer value to double' and luckily retrieving a meaningless(?) value, or being stuck in infinite loop. However, we can denote a constraint that 'if a is an integer, double' a is also an integer'.

Using Church encoding, it would be 'if the normal form of a is λf.λx.f(f...f(x)), then the one of double' a is also λf.λx.f(f...f(x))'. I agree that this is not strict enough, and that's the point my questions begin.


Is there any strict and general way to describe that kind of constraints?
If so, how powerful is it compared to type systems?


I'm sorry that my question is so ambigious. But I think that there could have been some similar approaches, and only links to them would be very helpful.
There's an old way of doing what you're asking for, coming from domain theory. Let $D$ be the collection of all values of the untyped $\lambda$-calculus. We can undestand $D$ to be some sort of a domain, or the set of closed normal terms, it does not really matter. We define a type to be a retraction $r : D \to D$, i.e., a continuous map (or a closed term if you want definable types) such that $r \circ r = r$. Such an $r$ represents the collection of its fixed points $D_r = \{x \in D \mid r(x) = x\}$. The map $r$ itself is a coercion from $D$ to $D_r$. Because it is a retraction, it does not do anything to elements of $D_r$.

Now, given any map $f : D \to D$ say that it maps $D_r$ to $D_q$ when $f = q \circ f \circ r$. This equation says that:


$f$ is already determined by its restriction $f{\restriction}_{D_r}$ to $D_r$ (because $f = f{\restriction}_{D_r} \circ r$),
the image of $f$ is contained in $D_q$ (because $f = q \circ f$).


Putting these two together, we see that $f$ can be thought of as going from $D_r$ to $D_q$ (it is important that $f$ does not carry any additional information about how to map elements outside $D_r$, or else we could  have several different functions that all act the same way on $D_r$).

Actually, any map $g : D \to D$ can be coerced to a map from $D_r$ to $D_q$ by the retraction $g \mapsto q \circ g \circ r$.

Let us see how this relates to your question. You would like to have a way of saying that a map $f$ maps integers to integers (I presume you mean natural numbers since you speak of Church numerals). So what we need is a map $r$ such that $r (r x) = x$ if, and only if, $x$ represents an integer. Once we have such a map we can express the fact that $f$ maps integers to integers with the equation $f = r \circ f \circ r$.

So it remains to write down a map $r$ in the untyped $\lambda$-calculus whose fixed points are Church numerals (and also some diverging terms which denote bottom). I think this might work:
$$r(x) = \mathtt{rec}\;\mathtt{Z}\;(\lambda n\,y \,. \mathtt{S}\,y)\;x,$$
where $\mathtt{rec}$ is a simple recursor over natural numbers, $\mathtt{Z}$ is zero and $\mathtt{S}$ is successor. Intuitively, speaking, if $x$ behaves like a natural number, then $r(x)$ will "rebuild" it into standard form $\mathtt{S}(\mathtt{S}(\cdots \mathtt{Z}))$.

We need to be a bit careful about how $\mathtt{rec}$ is implemented. It has to satisfy
$$\mathtt{rec}\;x\;f\;\mathtt{Z} = x$$
and
$$\mathtt{rec}\;x\;f\;(\mathtt{S}\,n) = f\;n\;(\mathtt{rec}\;x\;f\;n),$$
and it should "crash" when we feed it something that does not behave like a numeral.