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 futhark_f32_1d *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.