ATS/GTK Basics

ATS is a rich programming language equipped with a highly expressive type system for specifying and enforcing program variants. Both dependent and linear types are available in ATS to support practical programming. ATS/GTK is the API in ATS for GTK+, a comprehensive toolkit for building graphical user interfaces. There are already many on-line tutorials on using GTK (e.g., this one), and the reader may want to use them as references when studying the current one, which focuses on using types in ATS to facilitate safe and reliable programming with GTK. In particular, the reader may find that linear types in ATS can do wonders in terms of tracking resource usage statically and significantly reducing, if not completely eliminating, memory leaks.

A Simple Example: Hello, world!

The first program we present in this tutorial is given as follows:


%{^
extern
ats_void_type mainats (ats_int_type argc, ats_ptr_type argv) ;
%} // end of [%{^]

(* ****** ****** *)

staload "contrib/glib/SATS/glib.sats"
staload "contrib/glib/SATS/glib-object.sats"

(* ****** ****** *)

staload "contrib/GTK/SATS/gtk.sats"
staload "contrib/GTK/SATS/gtkclassdec.sats"

(* ****** ****** *)

extern
fun gtk_window_set_title {l:agz}
  (win: !gobjref (GtkWindow, l), title: string): void
  = "mac#atsctrb_gtk_window_set_title"
// end of [gtk_window_set_title]

(* ****** ****** *)

extern fun main1 (): void = "main1"
implement main1 () = () where {
//
  val win = gtk_window_new (GTK_WINDOW_TOPLEVEL)
  val () = gtk_window_set_title (win, "Hello, world!")
  val () = gtk_widget_set_size_request (win, (gint)200, (gint)200)
  val () = gtk_widget_show (win)
  val _sid = g_signal_connect0
    (win, (gsignal)"delete-event", G_CALLBACK(gtk_main_quit), (gpointer)null)
  // end of [val]
  val () = gtk_main ()
//
} // end of [main]

(* ****** ****** *)

implement main_dummy () = () // indicating that [main] is implemented externally

(* ****** ****** *)

%{$
ats_void_type
mainats (
  ats_int_type argc, ats_ptr_type argv
) {
  gtk_init ((int*)&argc, (char***)&argv) ; main1 () ; return ;
} // end of [mainats]
%} // end of [%{$]

The functions in the GTK package are declared in the file contrib/GTK/SATS/gtk.sats , which contains many subfiles, and the GTK class hierachy is declared in the file contrib/GTK/SATS/gtkclassdec.sats . Note that in this tutorial, a file name, if relative, is always relative to the ATS home directory (stored in the environment variable ATSHOME) unless it is specified otherwise.

The function mainats is the main function in ATS, which is called by the main function in C. For GTK+ programming in ATS, the function mainats is implemented externally as follows:


%{$
ats_void_type
mainats (
  ats_int_type argc, ats_ptr_type argv
) {
  gtk_init ((int*)&argc, (char***)&argv) ; main1 () ; return ;
} // end of [mainats]
%} // end of [%{$]

The function main1, which is implemented in ATS, plays the real role of the main function. The very reason for this design is due to the need to handle the fact that gtk_init may modify its arguments argc and argv.

We use gobjref for contructing types for g-objects, which is declared in the file contrib/glib/SATS/glib-object.sats as follows:


absviewtype gobjref (c:cls, l:addr) // a (counted) reference to a g-object.

Given a class C and an address L, gobject(C, L) is for a g-object located at L that is of class C. Note that gobject(C, L) is a viewtype, that is, it is linear.

In the following declaration, gtk_window_set_title is declared to be an external function of the name atsctrb_gtk_window_set_title:


extern
fun gtk_window_set_title {l:agz}
  (win: !gobjref (GtkWindow, l), title: string): void = "mac#atsctrb_gtk_window_set_title"
// end of [gtk_window_set_title]

Note that GtkWindow is a class (or more precisely, a class name) declared elsewhere. Obviously, the type assigned to gtk_window_set_title indicates that this function takes two arguments and returns void; the first argument is a linear reference to a g-object located at some address that is of the class GtkWindow, and it is kept available after function call; the second argument is a string. In the file contrib/GTK/SATS/gtk.cats , atsctrb_gtk_window_set_title is defined as follows:


#define atsctrb_gtk_window_set_title gtk_window_set_title

indicating that the function gtk_window_set_title in ATS is just the function of the same name in C. Of course, we could use gtk_window_set_title for atsctrb_gtk_window_set_title in the first place. However, the present style makes it more convenient for the sake of debugging. Please note that gtk_window_set_title is already declared in the API for GTK in ATS. The above declaration is presented solely for the purpose of illustraton. If we ever need a GTK+ function that is not yet available in the API, we can just follow the example by declaring it on the spot. After all, ATS shares with C the very same data representation.