While Loops

The while construct

while B do
  C
done

The boolean expression B is evaluated. If true, command C is executed and the loop repeats. If false, the while terminates (possibly without executing C even once). The construct always returns ().

Example: imperative list length

let tlopt = function
  | [] -> None
  | _ :: xs -> Some xs

let length xs =
  let lp = ref xs in
  let np = ref 0 in
  let fin = ref false in
  while not !fin do
    match tlopt !lp with
    | None -> fin := true
    | Some xs ->
        lp := xs;
        np := 1 + !np
  done;
  !np
(* val length : 'a list -> int = <fun> *)

This computes list length imperatively:

• lp holds the remaining unexamined list.
• np accumulates the count.
• fin signals when the list is exhausted.
• tlopt safely returns None for the empty list (avoiding an exception from tl).

The loop body either sets fin to terminate, or advances lp and increments np.

Comparison with tail recursion

While loop	Tail recursion
Uses mutable references	Uses accumulator arguments
Returns ()	Returns the accumulated value
Loop invariant describes state	Induction on recursive calls
More familiar to imperative programmers	More natural in functional style

Both achieve O(n) time and O(1) space. The choice is stylistic. OCaml compilers optimise tail recursion well, so the recursive version is typically preferred in idiomatic OCaml.

Loop invariants

A loop invariant is a property that holds:

1. Before the first iteration.
2. After each iteration.
3. When the loop terminates.

For length: the invariant is that !np is the number of elements examined so far, and !lp holds the unexamined suffix of the original list. When !lp is empty (fin = true), !np equals the total length.