Counting Change by Use of Exceptions

In Harper's book, section 12.2 we have a function which computes change from an arbitrary list of coin values:

exception Change                             (* 1 *)
fun change 0 = nil                           (* 2 *)
  | change nil = raise Change                (* 3 *)
  | change (coin::coins) amt =               (* 4 *)
if coin > amt then                           (* 5 *)
  change coins amt                           (* 6 *)
else                                         (* 7 *)
  (coin :: change (coin::coins) (amt-coin))  (* 8 *)
 handle Change => change coins amt           (* 9 *)

The idea is to proceed greedily, but if we get stuck, we undo the most recent greedy decision and proceed again from there.

I attempted to simulate evaluation of the example of change [5,2] 16 to see how the code works, but have gotten stuck:

coin	coins	amt	function call
5	[2]	16	5::change(5::[2]) 11
5	[2]	11	5::change(5::[2]) 6
5	[2]	6	5::change(5::[2]) 1
5	[2]	1	change([2]::amt) 1
2	[]	1	change([]::amt) 1
nil			`raise Change` which calls `handle Change` which calls `change coins amt` which is where I am lost on what happens next and with what values

I am guess that the line #8 gets called with change coins amt being equal to {{{change [2]

"Natural" Numbers in SML

Harper shows an efficient way to insure that a factorial function does not receive negative numbers:

exception Factorial
local
fun fact 0 = 1
| fact n = n * fact (n-1)
in
fun checked factorial n =
if n >= 0 then
fact n
else
raise Factorial
end

but my question is: can we create a whole number type and set the input and output type of this function to it?

Says AdamChlipala: Natural numbers are in the SML Basis as implementations of the WORD signature.