4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – frangio Aug 18 '16 at 8:23
6
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Max New Aug 24 '16 at 18:09
  • $\begingroup$ Wouldn't your informal statement be better stated as "q \circ f \circ r = f \circ r"? $\endgroup$ – Max New Aug 24 '16 at 18:46
  • 1
    $\begingroup$ 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$. $\endgroup$ – Andrej Bauer Aug 24 '16 at 19:34
  • $\begingroup$ 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? $\endgroup$ – Max New Aug 24 '16 at 22:08
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Aug 25 '16 at 9:06

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.