例: 線形リストの挿入ソート

fun{
a:t@ype
} insertionSort{n:nat}
  (xs: list_vt (a, n), cmp: cmp a): list_vt (a, n)
// end of [insertionSort]

fun{
a:t@ype
} insord
  {l0,l1,l2:addr}{n:nat}
(
  pf1: a @ l1
, pf2: list_vt (a, 0)? @ l2
| xs0: &list_vt (a, n) >> list_vt (a, n+1)
, nx0: list_vt_cons_unfold (l0, l1, l2), p1: ptr (l1), p2: ptr (l2)
, cmp: cmp (a)
) : void =
(
  case+ xs0 of
  | @list_vt_cons
      (x0, xs1) => let
      val sgn = compare<a> (x0, !p1, cmp)
    in
      if sgn <= 0 // HX: for stableness: [<=] instead of [<]
        then let
          val () = insord<a> (pf1, pf2 | xs1, nx0, p1, p2, cmp)
          prval () = fold@ (xs0)
        in
          // nothing
        end // end of [then]
        else let
          prval () = fold@ (xs0)
          val () = (!p2 := xs0; xs0 := nx0)
          prval () = fold@ (xs0)
        in
          // nothing
        end // end of [else]
      // end of [if]
    end // end of [list_vt_cons]
  | ~list_vt_nil () =>
    {
      val () = xs0 := nx0
      val () = !p2 := list_vt_nil ()
      prval () = fold@ (xs0)
    }
) (* end of [insord] *)

implement{a}
insertionSort
  (xs, cmp) = let
//
fun loop{m,n:nat}
(
  xs: list_vt (a, m)
, ys: &list_vt (a, n) >> list_vt (a, m+n)
, cmp: cmp (a)
) : void =
  case+ xs of
  | @list_vt_cons
      (x, xs1) => let
      val xs1_ = xs1
      val ((*void*)) =
        insord<a> (view@x, view@xs1 | ys, xs, addr@x, addr@xs1, cmp)
      // end of [va]
    in
      loop (xs1_, ys, cmp)
    end // end of [list_vt_cons]
  | ~list_vt_nil ((*void*)) => ()
//
var ys = list_vt_nil{a}()
val () = loop (xs, ys, cmp)
//
in
  ys
end // end of [insertionSort]

fun{
a:t@ype
} msort{n:nat} .<n>.
(
  xs: list_vt (a, n)
, n: int n, cmp: cmp(a)
) : list_vt (a, n) = let
//
// cutoff is selected to be 10
//
in
  if n > 10 then let
    val n2 = half(n)
    val n3 = n - n2
    var xs = xs // lvalue for [xs]
    val ys = split<a> (xs, n3)
    val xs = msort<a> (xs, n3, cmp)
    val ys = msort<a> (ys, n2, cmp)
    var res: List_vt (a) // uninitialized
    val () = merge<a> (xs, ys, res(*cbr*), cmp)
  in
    res
  end else insertionSort<a> (xs, cmp)
end // end of [msort]