Chapter 3. Types for Some Functions in Cairo

We now present some functions in cairo and the types assigned to them in ATS. These types often reveal a lot more information about the functions to which they are assigned than their counterparts in C.

The following function cairo_destroy is for destroying a cairo context:

fun cairo_destroy (cr: cairo_ref1): void

What this funtion really does is to decrease by 1 the reference count of the object referred to by its argument. The object is freed, that is, truly destroyed only if the new count becomes 0. Because cairo_ref1 is a linear type (or viewtype in ATS), if cairo_destroy(cr) is called, then cr can no longer be used as it is consumed: a linear value, that is, a value of a linear type, must be used once and only once. This point is made much clearer in the following example, where the function cairo_reference is presented:

fun cairo_reference {l:agz} (cr: !cairo_ref l): cairo_ref l

First, agz is a sort defined as follows:

sortdef agz = {l:addr | l > null}

Therefore, {l:agz} is simply a shorthand for {l:addr | l > null}. What cairo_reference does is to increase the reference count of its argument by 1. In the type assigned to cairo_reference, the symbol ! in front of cairo_ref indicates that the argument of the function cairo_reference is not consumed by a call to the function (and thus it can be used later). Clearly, the type also indicates that the value returned by cairo_reference(cr) is a reference pointing to the same location as cr does. If the symbol ! was omitted, the function would consume a cairo context and then return one, thus preserving reference count.

The following function cairo_create is for creating a cairo context:

fun cairo_create {l:agz} (sf: !cairo_surface_ref l): cairo_ref1

The type of this function indicates that it takes a reference to a cairo surface and returns a reference to a cairo context; the symbol ! indicates that the reference to the surface is preserved and thus is still available after the function being called; if the reference to the surface is no longer needed, it is necessary to call the function cairo_surface_destroy on the reference.

We can have another function cairo_create0 of the following type for creating a cairo context:

fun cairo_create0 {l:agz} (sf: cairo_surface_ref l): cairo_ref1

After calling cairo_create0 on a cairo surface, the surface is consumed, that is, it is no longer available for subsequent use, and therefore there is no need to destroy it by calling cairo_surface_destroy. If both cairo_create and cairo_create0 are provided to the programmer in a language like C, it can readily lead to memory leaks as one may mistakenly use cairo_create0 in place of cairo_create. This, however, is not an issue in ATS as such an error is surely caught during typechecking.

As various functions can modify the cario context they use, it is often necessary to save the state of a context so that the saved state can be restored at a later point. The functions for saving and restoring the state of a cairo context are given as follows:

fun cairo_save {l:agz} (cr: !cairo_ref l): (cairo_save_v l | void)
fun cairo_restore {l:agz} (pf: cairo_save_v l | cr: !cairo_ref l): void

The view constructor cairo_save_v is declared to be abstract:

absview cairo_save_v (l:addr) // abstract view generated by cairo_save

The simple idea behind cairo_save_v is this: Given a reference of the type cairo_ref(L) for some address L, a call to cairo_save on the reference returns a linear proof of the view cairo_save_v(L), and this proof must be consumed at some point by a call to cairo_restore on a reference of the type cairo_ref(L). In other words, calls to cairo_save and cairo_restore are guaranteed to be properly balanced in a well-typed ATS program. This is evidently a desirable feature given that balancing such calls can often be a onerous burden for the programmer programming in languages like C.