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?)

Answer 1

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

Answer 2

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.