SML: Value restriction error when recursively calling quicksort

I'm writing a quicksort function for an exercise. I already know of the 5-line functional quicksort; but I wanted to improve the partition by having it scan through the list once and return a pair of lists splitting the original list in half. So I wrote:

fun partition nil = (nil, nil)
  | partition (pivot :: rest) =
  let
    fun part (lst, pivot, (lesseq, greater)) =
      case lst of
           [] => (lesseq, greater)
         | (h::t) =>
             if h <= pivot then part (t, pivot, (h :: lesseq, greater))
             else part (t, pivot, (lesseq, h :: greater))
  in
    part (rest, pivot, ([pivot], []))
  end;

This partitions well enough. It gives me a signature val partition = fn : int list -> int list * int list. It runs as expected.

It's when I use the quicksort below that things start to break.

fun quicksort_2 nil = nil
  | quicksort_2 lst = 
let
  val (lesseq, greater) = partition lst
in
  quicksort_2 lesseq @ quicksort_2 greater
end;

I can run the above function if I eliminate the recursive calls to quicksort_2; but if I put them back in (to actually go and sort the thing), it will cease to run. The signature will be incorrect as well, giving me val quicksort_2 = fn : int list -> 'a list. The warning I receive when I call the function on a list is:

Warning: type vars not generalized because of value restriction are instantiated to dummy types (X1,X2,...)

What is the problem here? I'm not using any ref variables; the type annotation I've tried doesn't seem to help...

Solution

The main issue is that you're lacking the singleton list base case for your quicksort function. It ought to be

fun quicksort [ ] = [ ]
  | quicksort [x] = [x]
  | quicksort xs  = 
      let
        val (l, r) = partition xs
      in
        quicksort l @ quicksort r
      end

which should then have type int list -> int list given the type of your partition. We have to add this case as otherwise you'll never hit a base case and instead recurse indefinitely.

For some more detail on why you saw the issues you were having though:

The signature will be incorrect as well, giving me val quicksort_2 = fn : int list -> 'a list

This is because the codomain of your function was never restricted to be less general than 'a list. Taking a look at the possible branches in your original implementation we can see that in the nil branch you return nil (of most general type 'a list) and in the recursive case you get two 'a lists (per our assumptions thus far) and append them, resulting in an 'a list---this is fine so your type is not further restricted.

[Value Restriction Warning] What is the problem here? I'm not using any ref variables

The value restriction isn't really related to refs (though can often arise when using them). Instead it is the prohibition that anything polymorphic at the top level must be a value by its syntax (and thus precludes the possibility that a computation is behind a type abstractor at the top level). Here it is because given xs : int list we (ignoring the value restriction) have quicksort_2 xs : 'a list---which would otherwise be polymorphic, but is not a syntactic value. Correspondingly it is value restricted.