<p>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 <em>type</em> 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 <em>coercion</em> from $D$ to $D_r$. Because it is a retraction, it does not do anything to elements of $D_r$.</p>

<p>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:</p>

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

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

<p>Actually, <em>any</em> 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$.</p>

<p>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$.</p>

<p>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}))$.</p>

<p>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.</p>

CC BY-SA 3.0
2016-08-24T18:09:07.303Z
Isn't the requirement $f = q \circ f \circ r$ much stronger than "takes elements of $D_r$ to $D_q$" since it also talks about the rest of $D$? For example $id_D$ certainly takes elements of $D_r$ to $D_r$ but unless $r=id$, $id \neq r \circ id_D \circ r$. This has bothered me for a while about the Karoubi envelope, to me the more correct description would be "already enforces the coercion" but that seems like a less intuitively useful property.
Max New
CC BY-SA 3.0
2016-08-24T18:46:14.283Z
Wouldn't your informal statement be better stated as "q \circ f \circ r = f \circ r"?
Max New
CC BY-SA 3.0
2016-08-24T19:34:50.067Z
I edited the answer to explain why the requirement $f = q \circ f \circ r$ is exactly what we want. It is not correct to think of $id_D$ as taking elements of $D_r$ to $D_r$ because $id_D$ also carries information about how to map things outside $D_r$.
Andrej Bauer
CC BY-SA 3.0
2016-08-24T22:08:14.933Z
So is that property solely for the sake of having the right equality for $D_r \to D_q$? You could also take maps $\{ f : D \to D | q \circ f \circ r = f \circ r\} / (f = g \iff f \circ r = g \circ r)$ and it would be an equivalent space, right? Then this extra restriction is for the sake of having a canonical representative?
Max New
CC BY-SA 3.0
2016-08-25T09:06:59.203Z
Perhaps you get the same set, but I would need to think whether you get the same space. It is likely that you do because we have a canonical representative of each equivalence class, namely $q \circ f \circ r$ (which then essentially brings us back to what we have in the answer). The point of using retractions is that you get to do things with equations and fixed points, and you do not have to get your hands dirty with quotients and nasty stuff.
Andrej Bauer
CC BY-SA 3.0
2016-08-19T10:57:43.517Z
2016-08-24T19:33:25.980Z
2016-08-24T19:33:25.980Z
Andrej Bauer
<p>Defining a typed function in haskell,</p>

<pre><code>double::Integer-&gt;Integer
double a = a + a
</code></pre>

<p>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 <code>'if a is an integer, double' a is also an integer'</code>.</p>

<p>Using Church encoding, it would be <code>'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))'</code>. I agree that this is not strict enough, and that's the point my questions begin.</p>

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

<p>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.</p>

CC BY-SA 3.0
2016-08-18T08:23:27.903Z
You might want to look into contracts. Racket for example has a very complete, higher-order, contract system. Felleisen has quite some work on this, I believe. See for example "Contracts for Higher-Order Functions". I have not personally read it but I think it's in line with what you're thinking.
frangio
<lambda-calculus>
Translating typed functional language to untyped lambda calculus
toothpaste
# Translating typed functional language to untyped lambda calculus

(Asked by: username_0 on 2016-08-18)

Defining a typed function in haskell,
double::Integer->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.

**Tags:** lambda-calculus

> **Comments:**
> **username_1**: You might want to look into contracts. Racket for example has a very complete, higher-order, contract system. Felleisen has quite some work on this, I believe. See for example "Contracts for Higher-Order Functions". I have not personally read it but I think it's in line with what you're thinking.  

---

## 1 answers

### Answer by username_2 on 2016-08-19. Score: 6

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:

1. $f$ is already determined by its restriction $f{\restriction}\_{D\_r}$ to $D\_r$ (because $f = f{\restriction}\_{D\_r} \circ r$),
2. 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.

> **Comments:**
> **username_3**: Isn't the requirement $f = q \circ f \circ r$ much stronger than "takes elements of $D_r$ to $D_q$" since it also talks about the rest of $D$? For example $id_D$ certainly takes elements of $D_r$ to $D_r$ but unless $r=id$, $id \neq r \circ id_D \circ r$. This has bothered me for a while about the Karoubi envelope, to me the more correct description would be "already enforces the coercion" but that seems like a less intuitively useful property.  
> **username_3**: Wouldn't your informal statement be better stated as "q \circ f \circ r = f \circ r"?  
> **username_2**: I edited the answer to explain why the requirement $f = q \circ f \circ r$ is exactly what we want. It is not correct to think of $id_D$ as taking elements of $D_r$ to $D_r$ because $id_D$ also carries information about how to map things outside $D_r$.  
> **username_3**: So is that property solely for the sake of having the right equality for $D_r \to D_q$? You could also take maps $\{ f : D \to D | q \circ f \circ r = f \circ r\} / (f = g \iff f \circ r = g \circ r)$ and it would be an equivalent space, right? Then this extra restriction is for the sake of having a canonical representative?  
> **username_2**: Perhaps you get the same set, but I would need to think whether you get the same space. It is likely that you do because we have a canonical representative of each equivalence class, namely $q \circ f \circ r$ (which then essentially brings us back to what we have in the answer). The point of using retractions is that you get to do things with equations and fixed points, and you do not have to get your hands dirty with quotients and nasty stuff.  

---

