ML programmer's guide to ATS

In this guide, we don't aim to teach you programming in ATS (Applied Type System), but we need to tell you enough so that a seasoned ML programmer can quickly adjust to the terminology used in ATS and start reading existing ATS code.

Wonderful world of ATS

In ATS, it is useful to keep in mind that you will be programming in three worlds.

• Dynamics, the part that evaluates when you run the program. This is what programmers are most familiar with dealing with programming languages.
• Proofs, relates dynamic property with static property. Proofs are considered a dynamic part of the program but is stripped away after the compilation, so they are absent in run-time. The compiler checks your proof and then erases them before emitting code.
• Statics, the part evaluated by the compiler as part of type checking. The static part is a restricted form of programming so that evaluation of static expressions will always terminate, so type checking is decidable.

In ATS predecessor Dependent ML, the static world only sees a very limited presence of the dynamic world through dependent types. Each dynamic expression has a type that can be indexed with a static expression. Static constraints are collected from static expressions, and type checking involves solving these constraints to decide satisfiability.

In addition to dependent types, ATS also has proofs, which allow the static world to become more involved in dynamics by allowing programmers to write a dynamic expression and a proof term side-by-side to establish correspondence. Proofs can either be classical propositions, called props, or linear propositions (in the sense of linear logic—see margin note) called views.

However, more typically, .sats would define the type of a function to be implemented in .dats. In such case, the implementation in .dats does not need type annotation.

It is important to understand that, unlike ML, ATS type checker only performs very limited type inference. You have to explicitly annotate enough types (mostly arguments to a function) so ATS can reconstruct typing derivation.

Ecstatic statics

ATS is a bit like ML. You can define type and datatype.

From the SML code, there is a predefined type int, and here we define a new type name t aliased to int. We can define aliases to types parameterized by some type variables. We also define an option datatype that is parameterized by a type variable a. These identifiers are all static identifiers, in contrast to dynamic identifiers which are run-time variables.

In ATS, notice that type variables for datatype constructors need to be explicitly applied. For more information about datatype, see Datatypes in the ATS tutorial, but you may want to read the rest of this section first.

Type definition assigns a static identifier to a static expression with the sort "type", so typedef is a special case for stadef. The following two static declarations are almost the same.

The only difference is that typedef ensures that t will end up having the "type" sort, and stadef doesn't particularly care.

A type is one of the many sorts that a static expression or static identifier can be. Other sorts are:

• Ground sorts: int, bool, char, addr. They form the basis of dependent type indices.
• View, which are linear (in the sense of linear logic) propositions.
• Prop, which are classical propositions.
• Viewtype, which are linear types. It can be seen as a type combined with a view.

You can define a new sort using datasort. The first few lines of sllist.dats demonstrate how to define a sort that resembles a list. You can also alias sorts using sortdef, which also lets you piggy-back constraints to a sort called subset sort. See prelude/sortdef.sats for examples. A constraint is simply a static expression of a boolean sort.

For each of the type, view, prop, it is possible to alias, declare abstract quantities, and form algebraic constructors.

The static function nat_lt can be used whenever a bool sort is required. For example, if we want to constraint the range of a run-time integer argument:

• The built-in static identifier int is overloaded. It has two definitions, one of the sort "type", and one of the sort "int -> type". The second version is a dependent type integer, indexed by a static expression.
• This is a static expression of the "type" sort: int(3).
• We can restrict the integer type to a certain domain using existential quantifier with guard.

• Which defines a static function NatLt: int -> type. Given a static integer n, NatLt gives you a type that is a subset of integers from 0 to n - 1. The body of NatLt reads, "there exists i, which is of the int sort and that nat_lt(i, n) is true, yields a type int(i)."

We can then use the type NatLt(n) to write a function:

You can look at prelude/basics_sta.sats, which is part of ATS/Anariats, for the signatures of many built-in static operators. Notice that stadef allows many such operators to be overloaded. The fixity of many infix binary operators are defined in prelude/fixity.sats.

Atypical compound types

The first distinction is type with a fixed size, denoted simply as type, and type with an arbitrary but unknown size, denoted as t@ype. Values of type are like ML values, which has the same size as a machine pointer word. It can either be boxed or unboxed. Boxed values of type also resides on the managed (garbage collected) heap. Here are some examples of boxed values:

However, the ML types are too limited for system programming, which has to represent memory layout as a flat structure. This is where variables of t@ype would be useful. More often, memory layout of this form carries a view (linear resource) and a t@ype, and they are called viewt@ype altogether. Notice that t@ype is a subsort of viewt@ype, so anywhere viewt@ype is mentioned, we can give it just a t@ype. In fact, there is a static function sizeof(t) that has the same meaning in the C language, which has the static signature:

And the sizeof static function can be used for any t@ype and viewt@ype.

The boxed tuple, record, and list have analogy in the flat types as well.

But constructing flat values is a bit different. A flat value can reside either on the heap (like a boxed value) or on stack (which ML doesn't use for allocating data structure). This is discussed in another article, Manipulating flat memory.

Notice we can tell ATS that function_name will be called c_name when translated to C, though this is optional. This can be used to either:

1. Import an existing C function to ATS and decorate it with an ATS type, or
2. Export an ATS-implemented function to C with that name.

This has several important consequences.

• ATS function type can be mapped directly to C function type.
• ATS functions are always uncurried just like C functions.
• By default, functions cannot be used as closure, nor is partial application supported, unless specifically tagged as such (we will see tags below).

Adding guarded and assertion dependent types to the mix, we now have:

ATS (.sats)

fun function_name

    {forall quantifiers | guards} (x1: t1, ..., xn: tn):

    [exists quantifiers | asserts] t' =

  "c_name"

Where guards are static expressions of the bool sort written in terms of any forall quantifiers, and asserts are static expressions of the bool sort written in terms of any forall and exists quantifiers. Furthermore, t₁ ... t_n are static expressions of the type sort that can be written in terms of the for-all quantifiers, and t' is a static expression of the type sort that can be written in terms of any forall and exists quantifiers.

Now, we add proof terms to the mix too.

ATS (.sats)

fun function_name

    {forall quantifiers | guards} (pf1: prop1, ..., pfp: propp | x1: t1, ..., xn: tn):

    [exists quantifiers | asserts] (prop'1, ..., prop'q | t') =

  "c_name"

Notice that the uncurried arguments are now separated into two parts, proof variables and program variables. Proof variables will be erased once compilation finishes, leaving just the program variables in the resulting compiled program.

Finally, ATS uses decorated arrow type to keep track of side-effects as tags.

ATS (.sats)

fun function_name

    {forall quantifiers | guards} (pf1: prop1, ..., pfp: propp | x1: t1, ..., xn: tn)

  :<tag1, ..., tagk>

    [exists quantifiers | asserts] (prop'1, ..., prop'q | t') =

  "c_name"

If we were to write function type as a static expression (as opposed to function signature declaration like we've seen so far), the type expression would look like this:

ATS (static expression)

{forall...} (prop1, ..., propp | t1, ..., tn)

  -<tag1, ..., tagk> [exists...] (prop'1, ..., prop'q | t')

Tagged Arrow Type

The arrow type in ATS looks like "-<>", and the form -<tag₁, ..., tag_k> is an augmented arrow type with decoration. ATS currently recognizes the following tags for distinguishing various kind of functions:

• prf: proof function (will be erased after type checking).
• lin: a function that has to be called exactly once.
• fun: an ordinary function (default kind).
• cloptr: a closure that can be explicitly freed.
• cloref: a closure that is garbage collected.

As well as the following tags to track side-effects:

• exn: raises exceptions.
• ntm: possible non-termination.
• ref: sharing global memory reference.
• 0: no effects (pure).
• 1: all effects, including everything we don't know about yet.

In addition to the tags that distinguish function kinds, we can attach the 0 and 1 suffixes as a shorthand to indicate the presence or absence of effects. For example, cloref1 is a common tag for describing ML-style closure that is garbage collected and can have any side-effect (e.g. raises exceptions).

An example from stdio.h

What does a typical ATS function declaration look like? Here we show an example from the Standard C library that sports the following prototype.

char *fgets(char *s, int size, FILE *stream);

From the man page, "fgets() reads in at most one less than size characters from stream and stores them into the buffer pointed to by s. A '\0' is stored after the last character in the buffer." And that "fgets() returns s on success, and NULL on error or when end of file occurs while no characters have been read."

We now look at the ATS declaration, heavily commented and colored (orange is comment, cyan is keyword, and blue is static expression).

(* fgets_v describes the result of fgets, which can indicate either a

 * success or failure.

 *)

dataview fgets_v (sz:int, addr, addr) =

  | (* If success, location l is now a string buffer of size sz storing

     * a string of length n.

     *)

    {n:nat | n < sz} {l:addr | l <> null}

      fgets_v_succ(sz, l, l) of strbuf(sz, n) @ l

  | (* If failure, location l is still just sz number of bytes. *)

    {l:addr}

      fgets_v_fail(sz, l, null) of bytes(sz) @ l

fun fgets

    (* count is the number of bytes we want to read, and it has to fit

     * within sz, the size of buffer.

     *)

    {count, sz:int | 0 < count; count <= sz}

    (* fm is the static sort for file mode. *)

    {m:fm}

    (* l is for dependent type indexing for address of buffer. *)

    {l:addr}

    ( (* Proof that file mode implies read access. *)

      pf_mod: file_mode_lte(m, r),

      (* Linear proof that sz number of bytes is at l. *)

      pf_buf: bytes(sz) @ l

    | (* Argument, pointer indexed by location l. *)

      s: ptr(l),

      (* Argument, read at most count bytes. *)

      size: int(count),

      (* Argument, call by reference to FILE structure opened with

       * mode m.

       *)

      stream: &FILE(m)

    )

  :<>

    (* l' is the index for the return pointer. *)

    [l':addr]

    ( (* pf_buf is consumed, and this determines what it turns into

       * according to l'.

       *)

      fgets_v(sz, l, l')

    | (* Return pointer indexed by l'. *)

      ptr(l')

    ) =

  "fgets"

This example is based on libc/SATS/stdio.sats, part of ATS/Anariats, with slight modification and heavily annotated with comments. It may not be immediately apparent to the first-time reader, but there are some subtle points:

• We allow the actual buffer size (here denoted by the static variable sz) to be larger than what we tell fgets() to use (here denoted by the static variable count). This is the way fgets is formulated in libc/SATS/stdio.sats, but arguably it is not very common to tell fgets() not to use all of the buffer.
• If fgets() returns non-null, it must return the same pointer as before, but that pointer now should be interpreted as a strbuf, a string buffer holding zero terminated string of some length. Otherwise, the same view, bytes(sz) @ l, is given back. The only way to tell which case is the result of fgets() is by checking the pointer against null using an if-expression. It's a type error if you forget to check. If error checking gets tedius, libc/SATS/stdio.sats also has a version that raises an exception instead, called fgets_exn().

For your reference, this is what the above code looks like without comments.

dataview fgets_v (sz:int, addr, addr) =

  | {n:nat | n < sz} {l:addr | l <> null}

      fgets_v_succ(sz, l, l) of strbuf(sz, n) @ l

  | {l:addr}

      fgets_v_fail(sz, l, null) of bytes(sz) @ l

fun fgets

    {n, sz:int | 0 < n; n <= sz} {m:fm} {l:addr} (

      pf_mod: file_mode_lte(m, r), pf_buf: bytes(sz) @ l

    | s: ptr(l), size: int(n), stream: &FILE(m))

  :<>

    [l':addr] (fgets_v(sz, l, l') | ptr(l')) =

  "fgets"

TODO

• fn (non-recursive) vs fun (recursive) and termination metrics.