I wanted to give a small demonstration of ATS, partly to document a little bit of how to use atspkg, partly to show how to (safely) beat C's performance in ATS, and partly an example of how to parse command-line arguments in ATS.

We won't do a full implementation of wc here, but hopefully this post will give an indication of how one would do such a thing.

Installing Tooling

If you are on Linux or Mac, you can install atspkg with

curl -sSl https://raw.githubusercontent.com/vmchale/atspkg/master/bash/install.sh | bash -s

Otherwise, if you are a cabal user, you can install with

cabal new-install ats-pkg --symlink-bindir ~/.local/bin --happy-options='-gcsa' --alex-options='-g'

Next, you'll want to install pi, a project templating tool that has support for ATS. You can do this with

curl -LSfs https://japaric.github.io/trust/install.sh | sh -s -- --git vmchale/project-init

If you'd like to compile from source (you will have to install cargo):

cargo install project_init

Writing Code

Configuration

First, let's create a new project:

pi new ats ats-wc
cd ats-wc

We'll need to add linecount as a dependency. This is just a packaged version of a code example included in the examples; in general such a package will not exist, but there are many beautiful bits of code scattered about and you can collect them with relatively little effort.

Open up atspkg.dhall. You should see this:

let prelude = https://raw.githubusercontent.com/vmchale/atspkg/master/ats-pkg/dhall/atspkg-prelude.dhall
in prelude.default //
  { bin = 
    [ prelude.bin //
      { src = "src/ats-wc.dats"
      , target = "target/ats-wc" 
      }
    ]
  }

We'll add a field for our dependency to the outermost record:

let prelude = https://raw.githubusercontent.com/vmchale/atspkg/master/ats-pkg/dhall/atspkg-prelude.dhall
in prelude.default //
  { bin = 
    [ prelude.bin //
      { src = "src/ats-wc.dats"
      , target = "target/ats-wc" 
      }
    ]
    , dependencies = [ "ats-linecount" ]
  }

Great! Now we're ready to begin in earnest.

ATS

Open up src/ats-wc.dats. You should see this:

implement main0 () =
  println!("Hello, World!")

Since linecount already provides us with the function

fun line_count(s : string) : int

we simply need to provide a list of files and handle command-line arguments.

This turns out to be fairly involved in ATS. ATS provides two values to help us out here - argc (the number of arguments) and argv (their values as strings).

Our first step is to determine if a user passed the -h or --help flag. We also filter out any unrecognized command-line flags in this step.

fn should_help { n : nat | n > 0 }(argc : int(n), argv : !argv(n)) : bool =
  let
    fun loop {n:nat}{ m : nat | m < n } .<n-m>. (i : int(m), argc : int(n), argv : !argv(n)) :
      bool =
      let
        var s = argv[i]
      in
        ifcase
          | s = "-h" || s = "--help" => true
          | is_flag(s) => (prerr!("\33[31mError:\33[0m flag not recognized: '" + s + "'\n") ; exit(1))
          | i + 1 < argc => loop(i + 1, argc, argv)
          | _ => false
      end
  in
    loop(0, argc, argv)
  end

There's a lot going on here. The first thing to notice is the use of refinement types such as

{ n : nat | n > 0 }(argc : int(n), argv : !argv(n))

The syntax is a bit odd, but this is just a universal quantifier as a type. Crucially, ATS allows us to quantify over both int(n) and !argv(n) at the same time! This constraint means that argv (the array containing the values) has n elements, and also that argc is equal to n. The next bit is a little more exciting:

{n:nat}{ m : nat | m < n } .<n-m>. (i : int(m), argc : int(n), argv: !argv(n))

Here, we have two bound variables, m and n, with the constraint that m is less than n. This also means that i will be less than the number of elements in argv - crucially, this implies that argv[i] is safe.

The termination metric .<n-m>. is notable as well. Unlike Idris, ATS does not have a totality checker. Instead, we prove a function terminates by showing that some value decreases on every function call - in this case, n-m and hence argc - i.

The rest of the function is fairly typical ATS. We introduce a locally-scoped function loop and call it on some an initial index, ensuring safety with type-based static checks.

We can write a bare-bones help output as follows:

fun display_help() : void =
  println!("ats-wc - line counter written in ATS
\33[36mUSAGE:\33[0m ats-wc [FLAG] ... [FILE] ...
\33[36mFLAGS:\33[0m
    -h, --help             Display this help")

And then put this all together:

implement main0 (argc, argv) =
  if should_help(argc, argv) then
    display_help()

At this point, you can run

atspkg build
./target/ats-wc --help

and help information will be displayed.

The next bit we have to work out is how to parse rest of the command-line arguments. This doesn't involve any new concepts, but it is quite long.

fn cli_loop { n : nat | n > 1 }(argc : int(n), argv : !argv(n)) : void =
  let
    fn p_wc {n:nat}{ m : nat | m < n }(i : int(m), argv : !argv(n)) : int =
      let
        var s = argv[i]
      in
        let
          var c = line_count(s)
          val _ = if test_file_isdir(s) = 0 then
            println!(c, " ", s)
        in
          c
        end
      end
    fun loop {n:nat}{ m : nat | m < n } .. (i : int(m), argc : int(n), argv : !argv(n)) : int =
      ifcase
        | i + 1 < argc => let
          var total = p_wc(i, argv)
        in
          total + loop(i + 1, argc, argv)
        end
        | _ => p_wc(i, argv)
var total = loop(1, argc, argv)
  in
    if argc >= 3 then
      println!(total, " total")
  end

The main purpose of this function is simply printing out line number information for each file passed in as an argument, as well as a total if there are multiple files. The above function also filters out directories, so that they are not included in the output.

We can tie this all together by modifying main0 to:

implement main0 (argc, argv) =
  if should_help(argc, argv) then
    display_help()
  else
    if argc > 1 then
      cli_loop(argc, argv)
    else
      (prerr!("\33[31mError:\33[0m no input given\n") ; exit(1))

If all went well, you src/ats-wc.dats should look something like this:

#include "$PATSHOMELOCS/ats-linecount-0.2.2/lines.dats"
#include "share/atspre_staload_libats_ML.hats"
staload "libats/ML/SATS/string.sats"
fun display_help() : void =
  println!("ats-wc - line counter written in ATS
\33[36mUSAGE:\33[0m ats-wc [FLAG] ... [FILE] ...
\33[36mFLAGS:\33[0m
    -h, --help             Display this help")
fun is_flag(s : string) : bool =
  string_is_prefix("-", s)
fn should_help { n : nat | n > 0 }(argc : int(n), argv : !argv(n)) : bool =
  let
    fun loop {n:nat}{ m : nat | m < n } .<n-m>. (i : int(m), argc : int(n), argv : !argv(n)) :
      bool =
      let
        var s = argv[i]
      in
        ifcase
          | s = "-h" || s = "--help" => true
          | is_flag(s) => (prerr!("\33[31mError:\33[0m flag not recognized: '" + s + "'\n") ; exit(1))
          | i + 1 < argc => loop(i + 1, argc, argv)
          | _ => false
      end
  in
    loop(0, argc, argv)
  end
fn cli_loop { n : nat | n > 1 }(argc : int(n), argv : !argv(n)) : void =
  let
    fn p_wc {n:nat}{ m : nat | m < n }(i : int(m), argv : !argv(n)) : int =
      let
        var s = argv[i]
      in
        let
          var c = line_count(s)
          val _ = if test_file_isdir(s) = 0 then
            println!(c, " ", s)
        in
          c
        end
      end
    fun loop {n:nat}{ m : nat | m < n } .<n-m>. (i : int(m), argc : int(n), argv : !argv(n)) : int =
      ifcase
        | i + 1 < argc => let
          var total = p_wc(i, argv)
        in
          total + loop(i + 1, argc, argv)
        end
        | _ => p_wc(i, argv)
    var total = loop(1, argc, argv)
  in
    if argc >= 3 then
      println!(total, " total")
  end
implement main0 (argc, argv) =
  if should_help(argc, argv) then
    display_help()
  else
    if argc > 1 then
      cli_loop(argc, argv)
    else
      (prerr!("\33[31mError:\33[0m no input given\n") ; exit(1))

You can now build and run with

atspkg build
./target/ats-wc src/ats-wc.dats

Benchmarks

This is actually faster than wc. You can find more details here. I ran this benchmark on the full text of Ulysses.