I started work on my ATS math library recently; though I'm not sure it will be a wholehearted success, there were parts that deserve attention.

Let us first consider the following Haskell function to check primality:

hsIsPrime :: Int -> Bool hsIsPrime 1 = False hsIsPrime x = all ((/=0) . (x mod)) [2..m] where m = floor (sqrt (fromIntegral x :: Float))

This is actually quite nice, but it is also far from "as fast as C". We can rewrite this in ATS as follows:

#include "share/atspre_staload.hats"

staload "libats/libc/SATS/math.sats" staload UN = "prelude/SATS/unsafe.sats"

fun sqrt_int(k : intGt(0)) : [ m : nat ] int(m) = let var pre_bound: int = g0float2int(sqrt_float(g0int2float_int_float(k))) var bound: [ m : nat ] int(m) = $UN.cast(pre_bound) in bound end

fn is_prime(k : intGt(0)) : bool = case+ k of | 1 => false | k => begin let fun 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

As can be seen, this is a bit more involved. Some of this is to be expected as we prove termination, but some of it is simply due to using a lower-level language.

Note first the rather involved termination metric here - we use .<max(0,m-n)>. to ensure that it is well-founded. I learned this trick reading the ATS manual, and I actually encourage prospective learners to do this as well; it can be hard to get your hands on code samples.

Next, note the use of :<> in the type signature of loop. This is how ATS manages effects. You can have :<!ntm> for a function that may not terminate, :<!exn> for a function that could throw an exception, etc. So :<> simply means that the function is pure and total (that is, terminating).

Finally, note the use of an existential type in the declaration var bound: .... Existential types are a feature special to ATS; they are not present in any mainstream languages or even Idris. The type [ m : nat ] int(m) can then be passed as an argument to loop, though loop takes the universally quantified {m : nat} ... bound: int(m). Hence, we have a powerful technique that allows us to take a function on an ordinary int and nonetheless prove termination.

At this point, we can write a small Haskell wrapper. This is slightly dry, but I think it will be informative.


extern fun is_prime_ats { n : nat | n > 0 } : int(n) -> bool = "mac#"

implement is_prime_ats (n) = is_prime(n)

This is the necessary code on the ATS side of things; it simply exposes the function in the compiled library. We can compile it to C (placing it in cbits per Haskell packaging convention) with:

$ mkdir -p cbits $ patsopt -dd prime.dats -cc > cbits/prime.c

On the Haskell side we have the following:

module Numeric.NumberTheory where

import Data.Word import Foreign.C

foreign import ccall unsafe is_prime_ats :: CInt -> CBool

convertBool :: CBool -> Bool convertBool = go . fromIntegral where go :: Word8 -> Bool go 0 = False go 1 = True go _ = False

isPrime :: Int -> Bool isPrime = convertBool . is_prime_ats . fromIntegral

Our .cabal file will be a bit simple-minded. We simply add the following to our library stanza:

c-sources: cbits/primes.c include-dirs: /usr/local/lib/ats2-postiats-0.3.8/ccomp/runtime/ , /usr/local/lib/ats2-postiats-0.3.8/ ghc-options: -optc-mtune=native -optc-flto -optc-O3

Finally, we can benchmark both functions alongside one another:

Task Language Time
isPrime 2017 ATS 118.9 ns
isPrime 2017 Haskell 497.3 ns

This is exactly what we wanted - a 5x speedup compared to pure Haskell, with even more static guarantees to boot! With C, you can get the same speed (or perhaps even faster), but it always feels like an uncanny compromise. ATS allows us to write the functional code we want (with attendant safety guarantees) and still get the speed we need.