blog

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)
  end
fn 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.