Bluish Coder

Programming Languages, Martials Arts and Computers. The Weblog of Chris Double.


2017-01-19

Transitioning from ATS1 to ATS2

ATS is a programming language I've used a lot in the past. A new version was released a while ago, ATS2, that resulted in various library and language changes and I never got around to transitioning my code to it. Many of my existing posts on ATS are still relevant but some syntax has changed and many of my examples won't compile in the new system. I'm playing around with ATS 2 now and will note some of the major differences I've encountered in this post to get some of my existing ATS1 examples to build.

The first thing to note is that there's some extensive documentation for ATS2 compared to when I first started learning. This was very helpful in learning the differences.

Starting with a simple 'hello world' program:

implement main0() = print("Hello World\n")

Put in a 'hello.dats' file this can be compiled with:

$ patscc -o hello hello.dats
$ ./hello
Hello World

Notice that the main entry function is called main0. In ATS1 this was main. In ATS2 the use of main is to mirror the C main function in that it can take arguments and return a value:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

implement main(argc, argv) =
  if argc = 2 then
    (print("Hello "); print(argv[1]); print_newline(); 0)
  else
    (print("This program requires an argument.\n"); 1)

main takes the traditional argc and argv arguments that the C language main function takes. The function must return an integer value - in this example 0 for success and 1 for failure. Note the two #include statements. These are boilerplate used by ATS to enable the ATS compiler atsopt to gain access to certain external library packages and the definitions of various library functions.

$ patscc -o hello1 hello1.dats
$ ./hello1
This program requires an argument.
$ ./hello1 World
Hello World

In my Linear Datatypes in ATS article I showed an example of declaring a datatype and folding over it:

datatype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

fun {seed:t@ype}{a:t@ype} fold(f: (seed,a) -<> seed, s: seed, xs: list a): seed =
  case+ xs of
  | nil () => s
  | cons (x, xs) => fold(f, f(s, x), xs)

implement main() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = fold(add_int_int, 0, a)
  val c = fold(mul_int_int, 1, a)
  val () = printf("b: %d c: %d\n", @(b, c))
in
  ()
end

This won't compile in ATS2 due to:

  • add_int_int and mul_int_int don't exist in ATS2. They are replaced with g0int_add_int and g0int_mul_int.
  • printf doesn't exist in ATS2. I don't know of a replacement for this other than multiple print statements.
  • main needs to be main0.

The working ATS2 version becomes:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

datatype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

fun {seed:t@ype}{a:t@ype} fold(f: (seed,a) -<> seed, s: seed, xs: list a): seed =
  case+ xs of
  | nil () => s
  | cons (x, xs) => fold(f, f(s, x), xs)

implement main0() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = fold(g0int_add_int, 0, a)
  val c = fold(g0int_mul_int, 1, a)
  val _ = print("b: ")
  val _ = print_int (b)
  val _ = print (" c: ")
  val _ = print_int (c)
  val _ = print_newline()
in
  ()
end

Compiling this fails at the link stage however:

$ patscc -o test test.dats
/tmp/ccfgUdP6.o: In function `mainats_void_0':
t2_dats.c:(.text+0x138): undefined reference to `atsruntime_malloc_undef'
t2_dats.c:(.text+0x15c): undefined reference to `atsruntime_malloc_undef'
t2_dats.c:(.text+0x180): undefined reference to `atsruntime_malloc_undef'
t2_dats.c:(.text+0x1a4): undefined reference to `atsruntime_malloc_undef'
collect2: error: ld returned 1 exit status

The reason for this is the example uses dynamic memory allocation. ATS2 requires a command line argument to tell it to use the libc functions for allocating and freeing memory:

$ patscc -DATS_MEMALLOC_LIBC -o test test.dats
$ ./test
b: 10 c: 24

The same article shows a linear version of the datatype using dataviewtype:

dataviewtype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

fun {a:t@ype} free(xs: list a): void =
  case+ xs of
  | ~nil () => ()
  | ~cons (x, xs) => free(xs)

fun {seed:t@ype}{a:t@ype} fold(f: (seed,a) -<> seed, s: seed, xs: !list a): seed =
  case+ xs of
  | nil () => (fold@ xs; s)
  | cons (x, !xs1) => let val s = fold(f, f(s, x), !xs1) in fold@ xs; s end

implement main() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = fold(add_int_int, 0, a)
  val c = fold(mul_int_int, 1, a)
  val () = printf("b: %d c: %d\n", @(b, c))
in
  free(a)
end

Here the list type is linear. References to a list value can't be aliased and they must be explicitly consumed. In ATS2 this code now looks like:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

datavtype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

fun {a:t@ype} free(xs: list a): void =
  case+ xs of
  | ~nil () => ()
  | ~cons (x, xs) => free(xs)

fun {seed:t@ype}{a:t@ype} fold(f: (seed,a) -<> seed, s: seed, xs: !list a): seed =
  case+ xs of
  | nil () => (s)
  | cons (x, xs1) => let val s = fold(f, f(s, x), xs1) in s end


implement main0() = let
  val a = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = fold(g0int_add_int, 0, a)
  val c = fold(g0int_mul_int, 1, a)
  val _ = print("b: ")
  val _ = print_int (b)
  val _ = print (" c: ")
  val _ = print_int (c)
  val _ = print_newline()
in
  free a
end

This is mostly the same but the implementation of fold is simplified. There is no longer a need to use the "!" suffix when declaring the xs1 variable in the pattern match and the fold@ is not needed. In the cases where it is needed then an @ syntax seems to be used in the pattern match for ATS2:

fun {seed:t@ype}{a:t@ype} fold(f: (seed,a) -<> seed, s: seed, xs: !list a): seed =
  case+ xs of
  | nil () => (s)
  | @cons (x, xs1) => let val s = fold(f, f(s, x), xs1) in fold@ xs; s end

There is some discussion about this in the ATS tutorial but I need to look into it in detail to work out where it is needed now.

Another difference in this example is using datavtype instead of dataviewtype. The ATS2 examples I've seen consistently use the shorter word but the longer one still seems to work.

ATS2 makes more extensive use of templates. One thing that I found a pain point in ATS1 was dealing with higher order functions. ATS has multiple function types. There are functions that have no external environment (eg. plain C functions), closures which contain a pointer to an environment, linear closures where the closure envionment must be explicitly free'd, etc. (see closures in ATS for some examples). Writing higher order functions like map and filter would often require implementing a version for each type of function with duplicated boilerplate code.

The ATS2 library uses function templates specialized within the implementation of higher order functions to deal with this boilerplate. Here is an example of the technique adapted from Programming in ATS:

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"

datatype list (a:t@ype) =
  | nil (a)
  | cons (a) of (a, list a)

extern fun{a:t@ype}{b:t@ype} map$impl(x: a): b

fun{a:t@ype}{b:t@ype} map(xs: list a): list b = let
  fun loop(xs: list a): list b =
    case+ xs of
    | nil () => nil ()
    | cons(x, xs) => cons(map$impl<a><b>(x), loop(xs))
in
  loop(xs)
end

This implements a 'map' template function that takes a list of type a and returns a list of type b. It iterates over the list calling another template function called map$impl on each element and conses up the result. The map$impl function takes an a and returns a b. It is left unimplemented so far. The following is an implementation of a map that applies a function over the list:

fun{a:t@ype}{b:t@ype} map_fun(xs: list a, f: a -<fun> b) = let
  implement map$impl<a><b> (x) = f(x)
in
  map<a><b>(xs)
end

Here the map$impl function is implemented internally to map_fun to call the passed in function. The version that uses a closure does the same:

fun{a:t@ype}{b:t@ype} map_clo(xs: list a, f: a -<cloref> b) = let
  implement map$impl<a><b> (x) = f(x)
in
  map<a><b>(xs)
end

In this way the code that does the looping and mapping is implemented once in the map function and shared amongst the implementations that take the different function types. The caller doesn't need to know about templates to use it:

implement main0() = let
  val n = 5
  val a: list int = cons(1, cons(2, cons(3, cons(4, nil))))
  val b = map_fun(a, lam(x) => x * 2)
  val c = map_clo(a, lam(x) => x * n)

in
  ()
end

A lot of the ATS library implementation seems to take this approach, with template specialisation being used to extend it.

There are other additions to ATS2 that I haven't looked at yet. The constraint solver can be replaced with an external solver like Z3. There are backends for other languages, including JavaScript. There's a Try ATS online service for trying out the language and support for a C++ FFI.

I probably won't rewrite my existing ATS1 posts to be ATS2 compatible but will write about any changes needed to get things to compile if they're non-obvious.

Tags


This site is accessable over tor as hidden service mh7mkfvezts5j6yu.onion, or Freenet using key:
USK@1ORdIvjL2H1bZblJcP8hu2LjjKtVB-rVzp8mLty~5N4,8hL85otZBbq0geDsSKkBK4sKESL2SrNVecFZz9NxGVQ,AQACAAE/bluishcoder/-44/


Tags

Archives
Links