ATS is an obscure language, and perhaps justifiably so. It was exactly as I was warned (insane, idiosyncratic syntax; key features barely documented; no tutorials), but it was also beautiful, moving, and surprisingly practical.

I stumbled upon ATS after a period of disillusionment with Rust. Having become quite proficient in Haskell, Rust struck me as verbose and inexpressive. This became inexcusable when I wrote a parser for hask-replace and struggled to get performance that beat Haskell. I wanted a functional, fast language for polyglot.

ATS turned out to be a surprisingly good choice for polyglot; since there is relatively little information on systems programming in ATS, I figured I'd write up two short examples drawn from "real-world" use so that others might be able to experiment with functional systems programming as well.

Directory Streaming

Directory streaming in ATS is easier than doing it in Rust, provided you get past some of ATS' idiosyncrasies - note the use of the fnx keyword to denote a recursive function and the and keyword for a mutually recursive function.

When you get past that, it starts to look nicer. We lazily stream a directory's contents (recursively!), adding one to the counter every time we encounter a file. We filter out ./ and ../ so that the recursion actually terminates. There is some subtlety here - streamize_dirname_fname returns a linear stream - but once written the code is familiar to anyone with a bit of knowledge of functional programming.

#include "share/atspre_staload.hats"
#include "libats/ML/DATS/filebas_dirent.dats"
#include "libats/libc/DATS/dirent.dats"
staload "libats/ML/DATS/string.dats"
fun bad_dir(next: string) : bool =
  case next of
    | "." => true
    | ".." => true
    | _ => false
fnx step_stream(acc: int, s: string) : int =
  if test_file_isdir(s) = 1 then
    flow_stream(s, acc)
  else
    acc + 1
and flow_stream(s: string, init: int) : int =
  let
    var files = streamize_dirname_fname(s)
    // cloptr stands for "closure pointer", here written using a lambda
    var ffiles = stream_vt_filter_cloptr(files, lam x => not(bad_dir(x)))
  in
    stream_vt_foldleft_cloptr( ffiles
                             , init
                             , lam (acc, next) => step_stream(acc, s + "/" + next)
                             )
  end
implement main0() = ()

You can compile this example with

 $ patscc -DATS_MEMALLOC_LIBC stream.dats -o filecount -cleanaft

Unfortunately, finding these library functions was somewhat involved. I had to resort to ripgrep-ing the contents of /usr/local/lib/ats2-postiats-0.3.8/ in order to find streamize_dirname_fname and stream_vt_foldleft_cloptr, and then read the manual in order to understand how to use linear streams. Some of that was to be expected, as linear streams are a feature unique to ATS.

But we should still note that Rust doesn't really have any comparably nice way to accomplish this: recursion is (predictably) the best way to handle recursive directory descent.

String Padding

String padding is a bit trivial, but it is a nice example of how to use some of the advanced type system features that do not exist in any other systems programming language.

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#include "share/HATS/atslib_staload_libats_libc.hats"
%{^
#include "libats/libc/CATS/string.cats"
%}
staload "libats/ML/DATS/string.dats"
fnx right_pad { k: int | k >= 0 }{ m: int | m <= k } .<k>. (s: string(m), n: int(k)) : string =
  case+ length(s) < n of
    | true when n > 0 => right_pad(s, n - 1) + " "
    | _ => s
implement main0() = ()

The first thing to note is the use of refinement types here. They are enclosed in curly braces { k: int | k >= 0 } and function as universal quantifiers. You can read it as "for all integers \(k\) less than or equal to \(0\)" (define a function right_pad).

Next we note the use of dependent types. int(k) is a type for integers bounded by k. So { k: int | k >= 0 }(n : int(k)) means n is an integer that can be proven to be bounded at compile-time. Additionally, we can see that s must have length less than or equal to k - the function will never allow a string of length 22 to be padded to length 20, for example. This encodes something we know about the semantics of the function into the type system, preventing wasteful function calls.

Finally, we note something unique to ATS - the use of a termination metric, denoted .<k>.. This tells the compiler that k must strictly decrease on each function call; along with the condition imposed by { k : int | k >= 0 } this guarantees that the function is well-defined.

Coda

ATS is nowhere near as user-friendly as Rust, or even C. But it is nonetheless beautiful, vast, and in all probability the future of systems programming - just these short examples contain two features completely unique to ATS.