Do ML family compilers do any sophisticated optimization for tail calls?

Question

I (believe) the following function definition is tail-recursive:

fun is_sorted [] = true
  | is_sorted [x] = true
  | is_sorted (x::(y::xs)) =
    if x > y
       then false
       else is_sorted (y::xs)

Trivially, it's equivalent to the following declaration

fun is_sorted [] = true
  | is_sorted [x] = true
  | is_sorted (x::(y::xs)) = 
    (x <= y) andalso (is_sorted (y::xs))

Yet in this version the last step is to apply the 'andalso', so its not tail-recursive. Or it would seem so, except that since (at least Standard) ML (of NJ) uses short-circuit evaluation, the andalso is in fact /not/ the last step. So would this function have tail-call optimization? Or there any other interesting instances where an ML function that does not obviously use tail-recursion in fact gets optimized?

Answer 1

Note that

A andalso B

is equivalent to

if A then B else false

The SML language definition even defines it that way. Consequently, B is in tail position. No fancy optimisation necessary.

Answer 2

If I translate your second function to OCaml I get this:

let rec is_sorted : int list -> bool = function
| [] -> true
| [_] -> true
| x :: y :: xs -> x < y && is_sorted xs

This is compiled as a tail-recursive function by ocamlopt. The essence of the generated code (x86_64) is this:

        .globl      _camlAndalso__is_sorted_1008
_camlAndalso__is_sorted_1008:
        .cfi_startproc
.L103:
        cmpq        $1, %rax
        je  .L100
        movq        8(%rax), %rbx
        cmpq        $1, %rbx
        je  .L101
        movq        (%rbx), %rdi
        movq        (%rax), %rax
        cmpq        %rdi, %rax
        jge .L102
        movq        8(%rbx), %rax
        jmp .L103
        .align      2
.L102:
        movq        $1, %rax
        ret
        .align      2
.L101:
        movq        $3, %rax
        ret
        .align      2
.L100:
        movq        $3, %rax
        ret
        .cfi_endproc

As you can see there are no recursive calls in this code, just a loop.

(But other posters are right that OCaml doesn't do all that much in the way of sophisticated analysis. This particular result seems pretty straightforward.)