Here I present two ways to write Euler's totient function in ATS. First we write our primality check:

#include "share/atspre_staload.hats"staload "libats/libc/SATS/math.sats"
staload UN = "prelude/SATS/unsafe.sats"fn witness(n : int) :<> [ m : nat ] int(m) =
\$UN.cast(n)fn sqrt_int(k : intGt(0)) :<> [ m : nat ] int(m) =
let
var bound: int = g0float2int(sqrt_float(g0int2float(k)))
in
witness(bound)
endfn is_prime(k : intGt(0)) :<> bool =
case+ k of
| 1 => false
| k =>
begin
let
fnx loop {n : nat}{m : nat} .<max(0,m-n)>. (i : int(n), bound : int(m)) :<> bool =
if i < bound then
if k % i = 0 then
false
else
loop(i + 1, bound)
else
if i = bound then
if k % i = 0 then
false
else
true
else
true
in
loop(2, sqrt_int(k))
end
end

Note the use of witness to introduce the existential, which is needed in assure the compiler that sqrt_int(k) is positive and hence that the termination metric is well-founded (as sqrt_int(k) is used as an input to loop). The :<> in type signatures indicates a function that cannot have side-effects; in ATS this means that the function is guaranteed to terminate (a stronger condition than Haskell's purity).

Now we can implement the actual totient function. Our first example uses relatively straightforward recursion:

fn totient(n : intGte(1)) : int =
case+ n of
| 1 => 1
| n =>>
begin
let
fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m } .<k-m>. (i : int(m), n : int(k)) : int =
if i >= n then
if is_prime(n) then
n - 1
else
n
else
if n % i = 0 && is_prime(i) && i != n then
(loop(i + 1, n) / i) * (i - 1)
else
loop(i + 1, n)
in
loop(1, n)
end
end

And again using explicit stack allocation:

fn totient(n : intGte(1)) : int =
case+ n of
| 1 => 1
| n =>>
begin
let
fnx loop { k : nat | k >= 2 }{ m : nat | m > 0 && k >= m }{l : addr} .<k-m>. ( pf : !int @ l | i : int(m)
, n : int(k)
, res : ptr(l)
) : void =
if i >= n then
if is_prime(n) then
let
val () = !res := n - 1
in end
else
let
val () = !res := n - 1
in end
else
if n % i = 0 && is_prime(i) && i != n then
let
val () = !res := (!res / i) * (i - 1)
in
loop(pf | i + 1, n, res)
end
else
loop(pf | i + 1, n, res)      var res: int with pf = 1
val () = loop(pf | 1, n, addr@res)
in
res
end
end

Just for fun, here's how to implement the totient function in Haskell:

hsIsPrime :: (Integral a) => a -> Bool
hsIsPrime 1 = False
hsIsPrime x = all ((/=0) . (x mod)) [2..m]
where m = floor (sqrt (fromIntegral x :: Float))hsTotient :: (Integral a) => a -> a
hsTotient n = (n * product [ p - 1 | p <- ps ]) div product ps
where ps = filter (\k -> hsIsPrime k && n mod k == 0) [2..n]

The Haskell is a good deal slower, but there are certainly advantages in brevity as well.