[MLton] Fixed points in SML

[Wesley W. Terpstra]

I was reading http://en.wikipedia.org/wiki/Lambda_calculus and found  
their fixed-points interesting. Being able to do away with recursive  
definitions sounded interesting. I then tried to implement them in  
SML and had an adventure.

Let's start with the fixed point definition they gave:
Y = λ g. (λ x. g (x x)) (λ x. g (x x))
To save typing, I've changed this to:
Y = λ g. (λ x. (x x)) (λ x. g (x x))
... the savings will be more later.

A first blush at writing this in SML:
val Y = fn g => (fn x => x x) (fn x => g (x x))
... however, this fails to type-check because the type signature of  
the last lambda expression is:
(((((... ) -> 'a) -> 'a) -> 'a
which is impossible to write in SML.

So, I tried the following elaboration:
local
   datatype 'a t = T of 'a t -> 'a
in
   val Y : ('a -> 'a) -> 'a = fn g => (fn x => x (T x)) (fn (T x) =>  
g (x (T x)))
end
The idea here was that 'a t = ((((... ) -> 'a) -> 'a) -> 'a. Now the  
last lambda expression is possible.

However, this went into an infinite loop because SML is eager, and  
will expand the recursion out to infinity.

My next step was a simple iota expansion on the last lambda  
expression to defer evaluation:
local
   datatype 'a t = T of 'a t -> 'a
in
   val Y : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b = fn g => (fn x => x  
(T x)) (fn (T x) => fn y => g (x (T x)) y)
end
Then it worked!

val nonrecursive_factorial = fn f => fn x => if x = 0 then 1 else x *  
f (x - 1)
val factorial = Y nonrecursive_factorial

The point of my email is this: I believe both changes must be made to  
ANY fixed point algorithm implemented in SML. It seems to me that a  
datatype is necessary to implement recursion, and I challenge anyone  
to find a SML fixed-point implementation that doesn't use a datatype.  
It also seems to me that the iota expansion is necessary and that a  
fixed point function in SML must have type signature (('a -> 'b) ->  
'a -> 'b) -> 'a -> 'b. That is, a function with signature ('a -> 'a) - 
 > 'a can never terminate, even if 'a is a function like  
nonrecursive_factorial. Am I right? Anyone have a counter-example?