[MLton] Fixed points in SML

[Vesa Karvonen]

Quoting "Wesley W. Terpstra" <wesley at terpstra.ca>:
[...]
> 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. 

Below are two versions that use neither rec, fun, or datatype keywords
of SML.  Many variations of the below implementations are possible.
Whether or not they fulfill the requirements of the challenge depends
on what you mean by a "datatype".

val Y =
    fn f =>
       let
          val f' = ref (fn _ => raise Fail "Y")
          val f'' = fn x => !f' x
       in
          f' := f f''
        ; f''
       end

val fact = Y (fn fact => fn n => if n=0 then 1 else n * fact (n-1))
val 120 = fact 5


val Y =
    fn x =>
       let
          exception E of exn -> 'a -> 'b
       in
          (fn E p => x (fn a => p (E p) a))
             (E (fn E p => x (fn a => p (E p) a)))
       end

val fact = Y (fn fact => fn n => if n=0 then 1 else n * fact (n-1))
val 120 = fact 5

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

The only way to build recursive types in SML is either through
a recursive datatype or through exn.  The only way to build cyclic
data (ignoring functions) in SML is either trough a ref or an array
and a recursive type.

A function of type

   ('a -> 'a) -> 'a

can not return normally in SML.  Intuitively the reason for this is
that the function would need to create a value of any type and that
is impossible (in a strict language).  If we accept the type safety
of SML as given, then I guess a sufficient proof would be to argue
that if such a function would exist, then we could use it to (some
other) implement some other function that can not exist.  But now I
must get back to work...

-Vesa Karvonen