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/"

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.


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)


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.