TiML

(* Insertion sort with time complexity annotation *)
fun insertSort ['a] {m : Nat} (cmp : 'a * 'a -- $1 --> bool) (xs : 'a list) : 'a list using $m + 1 =
  case xs of
      [] => []
    | x :: xs' =>
      let
        val ys = insertSort cmp xs'
        fun insert ['a] {n : Nat} (x : 'a) (ys : 'a list) : 'a list using $n + 1 =
          case ys of
              [] => [x]
            | y :: ys' =>
              if cmp (x, y) then
                x :: ys
              else
                y :: insert x ys'
      in
        insert x ys
      end

(* Example usage *)
val sorted = insertSort (fn (a, b) => a < b) [3, 1, 4, 1, 5, 9, 2, 6]