blog

Compared with Rust, ATS provides better type safety at the boundaries; foreign functions and data structures can be used in a first-class way without sacrificing type safety.

This is due to ATS' viewtypes; integer-indexed/dependent linear types let us work safely with pointers.

As an example, we can safely call into a Futhark-generated API.

We use the mean function here; we export mean_f32 from Futhark, viz.

import "lib/github.com/diku-dk/statistics/statistics"
module stats_f32 = mk_statistics f32
entry mean_f32 = stats_f32.mean

The Futhark compiler then generates the follow C header files:

struct futhark_context_config ;
struct futhark_context_config *futhark_context_config_new(void);
void futhark_context_config_free(struct futhark_context_config *cfg);
struct futhark_context ;
struct futhark_context *futhark_context_new(struct futhark_context_config *cfg);
void futhark_context_free(struct futhark_context *ctx);
struct futhark_f32_1d ;
struct futhark_f32_1d *futhark_new_f32_1d(struct futhark_context *ctx,
                                          float *data, int64_t dim0);
int futhark_free_f32_1d(struct futhark_context *ctx,
                        struct futhark_f32_1d *arr);
int futhark_entry_mean_f32(struct futhark_context *ctx, float *out0, const
                           struct futharkf321d *in0);

There are some helper functions for allocating and freeing Futhark arrays.

The corresponding .sats file is:

absvt@ype fut_ctx_cfg
absvt@ype fut_ctx
absvt@ype f32_arr_1d
vtypedef futctxcfgptr = [ l : addr | l > null ] (fut_ctx_cfg @ l | ptr(l))
vtypedef futctxptr = [ l : addr | l > null ] (fut_ctx @ l | ptr(l))
absvt@ype f32_arr(m: int)
vtypedef f32_arrptr(m: int) = [ l : addr | l > null ] (f32_arr(m) @ l | ptr(l))
// technically should be int not int64 but nothing bad will happen on 64-bit architectures
fn futhark_new_f32_1d {m:nat}(p : !futctxptr, inp : !arrayptr(float, m), int(m)) : f32_arrptr(m) =
  "ext#"
fn futhark_free_f32_1d {m:nat}(p : !futctxptr, arr : f32_arrptr(m)) : int =
  "ext#"
fn futhark_entry_mean_f32 {m:nat}(p : !futctxptr, out : (&float? >> _), inp : !f32_arrptr(m)) : int =
  "ext#"

This API is safe; not only does it prevent double-frees with linear types, its use of integer-indexed refinement types with pointers ensures that we do not access past the end of the array even while we work with "raw" pointers.

Consider:

implement main0 () =
  {
    val arr0 = arrayptr($arrpsz{float}(1.0f, 2.0f, 3.0f))
    val ctx_cfg = futhark_context_config_new()
    val ctx = futhark_context_new(ctx_cfg)
    val fut_arr0 = futhark_new_f32_1d(ctx, arr0, 3)
    var ret: float
    val _ = futhark_entry_mean_f32(ctx, ret, fut_arr0)
    val () = println!(ret)
    val _ = futhark_free_f32_1d(ctx, fut_arr0)
    val () = futhark_context_free(ctx)
    val () = futhark_context_config_free(ctx_cfg)
    val () = arrayptr_free(arr0)
  }

If we replace

val arr0 = arrayptr($arrpsz{float}(1.0f, 2.0f, 3.0f))
⋮
val fut_arr0 = futhark_new_f32_1d(ctx, arr0, 3)

with

val arr0 = arrayptr($arrpsz{float}(1.0f, 2.0f, 3.0f))
⋮
val fut_arr0 = futhark_new_f32_1d(ctx, arr0, 2)

the program would fail to compile because arr0 has length 3 but 2 is not the size of the array arr0.

You can see the full example (an ATS library for GPU-accelerated statistics) here.

In this way, we can work with "raw" pointers via a safe API; this makes ATS unique even among languages like Rust.