Since SML is a functional language having as a unique control mechanism, then clearly we can define the factorial by just giving the recursive definition. A more, but this of course is such a trivial solution that it does not really give any more information. Here we a more sophisticated definition. We still exploit the implicit feature of Standard ML of providing a recursive definition, but this time we define the fixed point operator itself. As you see it has this type and we can define the function factorial by just taking the result of applying the fixed-point operator to the operator which defines the factorial. As you can see this argument here is not recursive any more. Rather than using the implicit recursive fixed-point operator provided by the system we can model it ourselves over an abstract data type. This is an abstract datatype which has just one constructor. It roles a function producing an object of type AB l. It has two operators: the unroll function, which when applied to a roll function produces the original function, and the fixed-point operator Y. If you look at this fixed-point operator, the way it is written is precisely the way you would write it in untyped l calculus. But since this is a typed language we have to go through this recursive abstract datatype and use the unroll and roll constructors in the right positions in order to be able to type it. | ![]() |