Function which applies its argument to itself?

Question

Consider the following SML function:

fn x => x x

This produces the following error (Standard ML of New Jersey v110.72):

stdIn:1.9-1.12 Error: operator is not a function [circularity]
  operator: 'Z
  in expression:
    x x

I can sort of see why this isn't allowed -- for one, I'm not really sure how to write down what its type would be -- but it's not completely nonsensical; for instance, I could pass the identity function to it and get it back.

Is there a name for this function? (Is there a way to express it in SML?)

If anyone's interested, I found that this is called the [U Combinator (see bottom of page)](http://www.ucombinator.org/), but couldn't find much more about it. — Ismail Badawi, Feb 06 '12 at 16:09
I didn't know it was called the U combinator, but as that page states, it's used to build the (apparently shortest) non-terminating program of the untyped lambda calculus that I put in my answer. — Fred Foo, Feb 06 '12 at 16:18

Fred Foo · Accepted Answer · 2012-02-06T16:05:14.170

7

There is no way to express this function in a language with an ML-like type system. Even with the identity function it wouldn't work, because the first x and the second in x x would have to be different instances of that function, of type (_a -> _a) -> (_a -> _a) and _a -> _a, respectively, for some type _a.

In fact, type systems are designed to forbid constructs like

(λx . x x) (λx . x x)

in the untyped lambda calculus. In the dynamically typed language Scheme, you can write this function:

(define (apply-to-self x) (x x))

and get the expected result

> (define (id x) x)
> (eq? (apply-to-self id) id)
#t

edited Feb 06 '12 at 16:05

answered Feb 06 '12 at 15:35

Fred Foo

355,277
75
744
836

“because the first x and the second in x x would have to be **different instances** of that function”: out of curiosity, what about languages with lazy evaluation? Beside of that, I'm not sure there is anything like “instance” in SML (except where there are side effects). The issue is just a typing issue (no type, often no sense, while not always). – Hibou57 Sep 17 '14 at 00:49
1

@Hibou57 By instance, I mean a different concretely-typed instantiation of a generic function. – Fred Foo Sep 20 '14 at 10:44

score 4 · Answer 2 · answered Feb 07 '12 at 05:42

Functions like this are often encountered in fixed-point combinators. e.g. one form of the Y combinator is written λf.(λx.f (x x)) (λx.f (x x)). Fixed-point combinators are used to implement general recursion in untyped lambda calculus without any additional recursive constructs, and this is part of what makes untyped lambda calculus Turing-complete.

When people developed simply-typed lambda calculus, which is a naive static type system on top of lambda calculus, they discovered that it was no longer possible to write such functions. In fact, it is not possible to perform general recursion in simply-typed lambda calculus; and thus, simply-typed lambda calculus is no longer Turing-complete. (One interesting side effect is that programs in simply-typed lambda calculus always terminate.)

Real statically-typed programming languages like Standard ML need built-in recursive mechanisms to overcome the problem, such as named recursive functions (defined with val rec or fun) and named recursive datatypes.

It is still possible to use recursive datatypes to simulate something like what you want, but it is not as pretty.

Basically, you want to define a type like 'a foo = 'a foo -> 'a; however, this is not allowed. You instead wrap it in a datatype: datatype 'a foo = Wrap of ('a foo -> 'a);

datatype 'a foo = Wrap of ('a foo -> 'a);
fun unwrap (Wrap x) = x;

Basically, Wrap and unwrap are used to transform between 'a foo and 'a foo -> 'a, and vice versa.

Whenever you need to call a function on itself, instead of x x, you have to explicitly write (unwrap x) x (or unwrap x x); i.e. unwrap turns it into a function that you can then apply to the original value.

P.S. Another ML language, OCaml, has an option to enable recursive types (normally disabled); if you run the interpreter or compiler with the -rectypes flag, then it is possible to write things like fun x -> x x. Basically, behind the scenes, the type-checker figures out the places where you need to "wrap" and "unwrap" the recursive type, and then inserts them for you. I am not aware of any Standard ML implementation that has similar recursive types functionality.

“I am not aware of any Standard ML implementation that has similar recursive types functionality”: the definition of SML does not allow it, so no implementation will ever have this. The need to wrap it in a data‑type may makes sense. Looking at a type definition like `'a f = 'a f -> 'a` makes me think it's a rewrite rule or an evaluation more than a type. But may be I'm biased on this. — Hibou57, Sep 17 '14 at 00:58

Function which applies its argument to itself?

2 Answers2

Linked