Introduction

Programming is difficult. It's mostly dealing with bugs (introduced by yourself or by others), so don't expect this book to make your life easier (it will probably make your life harder).

ATS is a programming language, and what makes it outstanding is the synthesis between the usual programming (where you issue commands to a computing machine) and proving theorems about behavior of the programs you write. In the latter case you struggle with your own understanding of why your program is even supposed to work, and then explaining your reasoning the the typechecker and the constraint solver in a very rigorous way.

Let's address this question: why prove that your program works? Traditionally you would write (and then maintain) a set of tests that exercise parts of your program to ensure things work as intended. However, some kinds of behavior are difficult to test, which is where proofs help.

In C programming, it is usually the case that bugs can have catastrophic consequences. Then it makes sense to act proactively and prevent bugs from ever occurring, instead of dealing with the consequences. This is where proofs can help, too.

This book is aimed to help C programmers pick up the skills necessary to use ATS on a daily basis. We assume that the reader has the following:

  • knowledge of C programming (so we don't have to reiterate what other books can explain)
  • knowledge of mathematics (so we can use things like sets and functions to ease explanations)
  • knowledge of Linux command line scripting (so you don't have much trouble installing ATS, compiling to from sources, and running)

Getting started

In the spirit of "The C Programming Language" by Kernighan and Ritchie, let's write the first program that simply prints the words "hello, world".

TODO: explain the usage of @vmchale's tool

In ATS, the program to print "hello, world" is

#include "utils/atspre_staload.hats"
implement main0 () = println!("hello, world")

Next, we write a program that uses the formulaC = (5/9)(F-32)to print the table of Fahrenheit temperatures and their Celsius equivalents. The program still consists of the main function, but uses several other functions to solve subproblems.

#include "share/atspre_staload.hats"

fun to_celsius (fahr: int): int = 5 * (fahr-32) / 9

implement main0 () = let
  val lower = 0
  val upper = 300
  val step = 20
  fun aux (fahr: int): void = let
  in
    if fahr <= upper then let
      val celsius = to_celsius fahr
    in
      println!(fahr, "\t", celsius);
      aux (fahr + step)
    end
  end
in
  aux (lower)
end

Let's break it down.

FIXME: how to refer to *lines* or *fragments of code* in the snippet above?

  • fun is a keyword for declaring a function and providing it with a body in one go
    • the line fun to_celsius (fahr: int): int = defines a function namedto_celsiusthat takes one argument named fahr of type int and returns some other value of type int
    • the function body is defined after the=sign
  • implementis a keyword for providing the body for an already-declared function
    • main0 is a special function that acts as an entry point to the program, like main in C
    • main0 doesn't take any parameters and it doesn't return any error code, either

  • valis a keyword for declaring a value (or, "binding" the result of evaluation of the right-hand side to a variable)

    • the line val celsius = to_celsius fahr evaluates to_celsius fahrand puts it into a new variable named celsius

  • let is a keyword for declaring a set of variables to be used in the block delimited by in and end

    • for instance, aux (lower) refers to aux that is defined in the precedinglet-inblock

  • ifworks the same as in C, but you don't have to put parenthesis anywhere

    • i.e. if (fahr <= upper) ...works just as well in this case
    • calling a function requires parentheses if a function takes more than one argument

  • ATS doesn't provide the C printffunction, and the call toprintln!is actually a macro call. For now, it suffices to say that the expression println!(fahr, "\t", celsius)is rewritten into print_int(fahr); print_string("\t"); print_int(celsius); print_newline ()

Note that val-variables in ATS are immutable, and therefore it is required that you specify the right-hand side! Looping constructs are supported, but it is often much easier to use tail-recursive functions instead.

Since we are C programmers, we can write the following program:

#include "share/atspre_staload.hats"

fun to_celsius (fahr: int): int = 5 * (fahr-32) / 9

implement main0 () = {
  val lower = 0
  val upper = 300
  val step = 20
  var fahr: int = lower
  var celsius: int = 0
  val () =
    while (fahr <= upper) {
      val () = celsius := to_celsius fahr
      val () = println!(fahr, "\t", celsius);
      val () = fahr := fahr + step
    }
}

The syntax { ... } defines a block of declarations (a block is an expression that evaluates to an element of voidtype). As in let, every declaration "binds" the result of evaluating its right-hand side to name given on the left-hand side.

  • the keyword var declares a mutable variable, and the part the = ... is optional in this case (but we nevertheless use it here)
  • whileis a looping construct, it needs two expressions, the condition and the body, which work the same as in C

ASIDE: with ATS you can write the simple version & only refine it if necessary!

At this point, let's talk about printf, in particular the things that make it prone to various failures. To recall, the first argument

of printf, i.e. the format string, defines the order and the type of the rest of the arguments. For instance, the format string "%d\t%d"requires that an integer is passed in, followed by another integer. If you were to pass just one integer, things would go kaboom! Not only that, but if you were to pass, say, a char*(which may have the same size as int, depending on the architecture of the target CPU), you'd see the bits of the pointer being misinterpreted as an integer.

In ATS, it is possible to express the preconditions on the calls to printf that are safe (yeah, every invocation of such a function in ATS would be safe). However, this makes usage of printfdifficult for programmer (dealing with complex types and proofs is a headache). Therefore, we make do with a macro println! or print!, that stands for successive invocations of different printing functions, one per argument.

The program just written contains a serious issue: the use of integer arithmetic. Let's rewrite it using floating-point arithmetic.

#include "share/atspre_staload.hats"

fun to_celsius (fahr: float): float = (5.0f/9.0f) * (fahr-32.0f)

implement main0 () = {
  val lower = 0
  val upper = 300
  val step = 20
  var fahr: int = lower
  var celsius: float = 0.0f
  val () =
    while (fahr <= upper) {
      val () = celsius := to_celsius ((i2f)fahr)
      val () = println!(fahr, "\t", celsius);
      val () = fahr := fahr + step
    }
}

ATS doesn't have any implicit coercion rules, so we have to use i2f to perform explicit integer to float conversion. Note that both floats and ints use the same operator syntax; this is accomplished with these language constructs:

  • symbols: it's a name given to an identifier permissible by the lexical syntax; e.g. +, -, *are symbols defined in theprelude (aka standard library)
    • we stress here that the standard arithmetic operators provided by prelude are not hard-wired into ATS
  • overloading: a symbol may stand for multiple different functions, the compiler performs disambiguation
  • infix operators: it is allowed to declare infix operators and specify associativity and precedence rules

The primitive types int and float are basically opaque (*abstract*) types. Expressions involving these types are rewritten by the compiler to mean the usual function calls, according to the rules specified by the programmer. For instance:

  • 5.0f / 9.0f is rewritten by compiler into div_float_float(5.0f,9.0f)
  • fahr-32.0f is rewritten by compiler into sub_float_float(fahr, 32.0f)

results matching ""

    No results matching ""