Such functions are often found in fixed-point combinators. for example, one form of Y combinator is written λf.(λx.f (xx)) (λx.f (xx)) . Fixed-point combinators are used to implement general recursion in an untyped lambda calculus without any additional recursive constructs, and this is part of what the untyped Turing-complete lambda calculus does.
When people developed a simply typed lambda calculus , which is a naive static type system at the top of the lambda calculus, they found that it was not possible to write such functions. In fact, it is not possible to perform general recursion in a simply typed lambda calculus; and therefore, a simple typed lambda calculus is no longer Turing. (One interesting side effect is that programs in simply typed lambda calculus always end.)
In real statically typed programming languages such as Standard ML, built-in recursive mechanisms are needed to solve the problem, such as named recursive functions (defined using val rec or fun ) and called recursive data types.
You can still use recursive data types to mimic something like what you want, but it's not so pretty.
Basically, you want to define a type of type 'a foo = 'a foo -> 'a ; however, this is not permitted. Instead, you transfer it as data: 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 convert between 'a foo and 'a foo -> 'a and vice versa.
Whenever you need to call a function yourself, instead of xx , you must explicitly write (unwrap x) x (or unwrap xx ); those. unwrap turns it into a function that can then be applied to the original value.
PS Another ML language, OCaml, has the ability to enable recursive types (usually disabled); if you run an interpreter or compiler with the -rectypes flag, then you can write things like fun x -> xx . Basically, behind the scenes, the type controller determines where you need to “wrap” and “expand” the recursive type, and then insert them for you. I do not know of any standard implementation of ML that has similar functions of recursive types.