(* The example from the 'Dependent types' subsection of \cite[p. 66]{KennedyThesis}. Inconsequentially modified because Stardust doesn't do numeric patterns. Also, the dependent universal quantifier in Kennedy's proposed type corresponds to an -all- plus an arrow. *) ; (*[ val power : -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*) fun power n x = if n = 0 then 1.0 else if n < 0 then 1.0 / power (~n) x else x * power (n-1) x (* Some buggy versions follow (and shadow the correct version!) *) (*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*) fun power n x = if n = 0 then 1.0 else if n < 0 then 1.0 / power (~n) x else x * x * power (n-1) x (* BUG *) (*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*) fun power n x = if n = 0 then 1.0 else if n < 0 then 1.0 / power (n-1) x (* BUG *) else x * power (n-1) x (*[ val power :! -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*) fun power n x = if n = 0 then 1.0 else if n < 0 then 1.0 / power (~n) x else power (n-1) x (* BUG *) (*[ val power : -all d : dim- -all n : int- int(n) -> real(d) -> real(d^n) ]*) fun power n x = if n = 0 then 1.0 else if n < 0 then 0.0 / power (~n + 3) x (* Two bugs, but well typed since zero has any dimension *) else x * power (n-1) x