| language | contributors | filename | |||
|---|---|---|---|---|---|
ATS |
|
learnats.dats |
ATS is a low-level functional programming language. It has a powerful type system which lets you write programs with the same level of control and efficiency as C, but in a memory safe and type safe way.
The ATS type system supports:
- Full type erasure: ATS compiles to efficient C
- Dependent types, including LF and proving metatheorems
- Refinement types
- Linearity for resource tracking
- An effect system that tracks exceptions, mutation, termination, and other side effects
This tutorial is not an introduction to functional programming, dependent types, or linear types, but rather to how they all fit together in ATS. That said, ATS is a very complex language, and this tutorial doesn't cover it all. Not only does ATS's type system boast a wide array of confusing features, its idiosyncratic syntax can make even "simple" examples hard to understand. In the interest of keeping it a reasonable length, this document is meant to give a taste of ATS, giving a high-level overview of what's possible and how, rather than attempting to fully explain how everything works.
You can try ATS in your browser, or install it from http://www.ats-lang.org/.
// Include the standard library
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
// To compile, either use
// $ patscc -DATS_MEMALLOC_LIBC program.dats -o program
// or install the ats-acc wrapper https://github.com/sparverius/ats-acc and use
// $ acc pc program.dats
// C-style line comments
/* and C-style block comments */
(* as well as ML-style block comments *)
/*************** Part 1: the ML fragment ****************/
val () = print "Hello, World!\n"
// No currying
fn add (x: int, y: int) = x + y
// fn vs fun is like the difference between let and let rec in OCaml/F#
fun fact (n: int): int = if n = 0 then 1 else n * fact (n-1)
// Multi-argument functions need parentheses when you call them; single-argument
// functions can omit parentheses
val forty_three = add (fact 4, 19)
// let is like let in SML
fn sum_and_prod (x: int, y: int): (int, int) =
let
val sum = x + y
val prod = x * y
in (sum, prod) end
// 'type' is the type of all heap-allocated, non-linear types
// Polymorphic parameters go in {} after the function name
fn id {a:type} (x: a) = x
// ints aren't heap-allocated, so we can't pass them to 'id'
// val y: int = id 7 // doesn't compile
// 't@ype' is the type of all non-linear potentially unboxed types. It is a
// supertype of 'type'.
// Templated parameters go in {} before the function name
fn {a:t@ype} id2 (x: a) = x
val y: int = id2 7 // works
// can't have polymorphic t@ype parameters
// fn id3 {a:t@ype} (x: a) = x // doesn't compile
// explicity specifying type parameters:
fn id4 {a:type} (x: a) = id {a} x // {} for non-template parameters
fn id5 {a:type} (x: a) = id2<a> x // <> for template parameters
fn id6 {a:type} (x: a) = id {..} x // {..} to explicitly infer it
// Heap allocated shareable datatypes
// using datatypes leaks memory
datatype These (a:t@ype, b:t@ype) = This of a
| That of b
| These of (a, b)
// Pattern matching using 'case'
fn {a,b: t@ype} from_these (x: a, y: b, these: These(a,b)): (a, b) =
case these of
| This(x) => (x, y) // Shadowing of variable names is fine; here, x shadows
// the parameter x
| That(y) => (x, y)
| These(x, y) => (x, y)
// Partial pattern match using 'case-'
// Will throw an exception if passed This
fn {a,b:t@ype} unwrap_that (these: These(a,b)): b =
case- these of
| That(y) => y
| These(_, y) => y
/*************** Part 2: refinements ****************/
// Parameterize functions by what values they take and return
fn cool_add {n:int} {m:int} (x: int n, y: int m): int (n+m) = x + y
// list(a, n) is a list of n a's
fun square_all {n:int} (xs: list(int, n)): list(int, n) =
case xs of
| list_nil() => list_nil()
| list_cons(x, rest) => list_cons(x * x, square_all rest)
fn {a:t@ype} get_first {n:int | n >= 1} (xs: list(a, n)): a =
case+ xs of // '+' asks ATS to prove it's total
| list_cons(x, _) => x
// Can't run get_first on lists of length 0
// val x: int = get_first (list_nil()) // doesn't compile
// in the stdlib:
// sortdef nat = {n:int | n >= 0}
// sortdef pos = {n:int | n >= 1}
fn {a:t@ype} also_get_first {n:pos} (xs: list(a, n)): a =
let
val+ list_cons(x, _) = xs // val+ also works
in x end
// tail-recursive reverse
fun {a:t@ype} reverse {n:int} (xs: list(a, n)): list(a, n) =
let
// local functions can use type variables from their enclosing scope
// this one uses both 'a' and 'n'
fun rev_helper {i:nat} (xs: list(a, n-i), acc: list(a, i)): list(a, n) =
case xs of
| list_nil() => acc
| list_cons(x, rest) => rev_helper(rest, list_cons(x, acc))
in rev_helper(xs, list_nil) end
// ATS has three context-dependent namespaces
// the two 'int's mean different things in this example, as do the two 'n's
fn namespace_example {n:int} (n: int n): int n = n
// ^^^ sort namespace
// ^ ^^^ ^ ^^^ ^ statics namespace
// ^^^^^^^^^^^^^^^^^ ^ ^ value namespace
// a termination metric can go in .< >.
// it must decrease on each recursive call
// then ATS will prove it doesn't infinitely recurse
fun terminating_factorial {n:nat} .<n>. (n: int n): int =
if n = 0 then 1 else n * terminating_factorial (n-1)
/*************** Part 3: the LF fragment ****************/
// ATS supports proving theorems in LF (http://twelf.org/wiki/LF)
// Relations are represented by inductive types
// Proofs that the nth fibonacci number is f
dataprop Fib(n:int, m:int) =
| FibZero(0, 0)
| FibOne(1, 1)
| {n, f1, f2: int} FibInd(n, f1 + f2) of (Fib(n-1,f1), Fib(n-2,f2))
// Proved-correct fibonacci implementation
// [A] B is an existential type: "there exists A such that B"
// (proof | value)
fun fib {n:nat} .<n>. (n: int n): [f:int] (Fib(n,f) | int f) =
if n = 0 then (FibZero | 0) else
if n = 1 then (FibOne | 1) else
let
val (proof1 | val1) = fib (n-1)
val (proof2 | val2) = fib (n-2)
// the existential type is inferred
in (FibInd(proof1, proof2) | val1 + val2) end
// Faster proved-correct fibonacci implementation
fn fib_tail {n:nat} (n: int n): [f:int] (Fib(n,f) | int f) =
let
fun loop {i:int | i < n} {f1, f2: int} .<n - i>.
(p1: Fib(i,f1), p2: Fib(i+1,f2)
| i: int i, f1: int f1, f2: int f2, n: int n
): [f:int] (Fib(n,f) | int f) =
if i = n - 1
then (p2 | f2)
else loop (p2, FibInd(p2,p1) | i+1, f2, f1+f2, n)
in if n = 0 then (FibZero | 0) else loop (FibZero, FibOne | 0, 0, 1, n) end
// Proof-level lists of ints, of type 'sort'
datasort IntList = ILNil of ()
| ILCons of (int, IntList)
// ILAppend(x,y,z) iff x ++ y = z
dataprop ILAppend(IntList, IntList, IntList) =
| {y:IntList} AppendNil(ILNil, y, y)
| {a:int} {x,y,z: IntList}
AppendCons(ILCons(a,x), y, ILCons(a,z)) of ILAppend(x,y,z)
// prfuns/prfns are compile-time functions acting on proofs
// metatheorem: append is total
prfun append_total {x,y: IntList} .<x>. (): [z:IntList] ILAppend(x,y,z)
= scase x of // scase lets you inspect static arguments (only in prfuns)
| ILNil() => AppendNil
| ILCons(a,rest) => AppendCons(append_total())
/*************** Part 4: views ****************/
// views are like props, but linear; ie they must be consumed exactly once
// prop is a subtype of view
// 'type @ address' is the most basic view
fn {a:t@ype} read_ptr {l:addr} (pf: a@l | p: ptr l): (a@l | a) =
let
// !p searches for usable proofs that say something is at that address
val x = !p
in (pf | x) end
// oops, tried to dereference a potentially invalid pointer
// fn {a:t@ype} bad {l:addr} (p: ptr l): a = !p // doesn't compile
// oops, dropped the proof (leaked the memory)
// fn {a:t@ype} bad {l:addr} (pf: a@l | p: ptr l): a = !p // doesn't compile
fn inc_at_ptr {l:addr} (pf: int@l | p: ptr l): (int@l | void) =
let
// !p := value writes value to the location at p
// like !p, it implicitly searches for usable proofs that are in scope
val () = !p := !p + 1
in (pf | ()) end
// threading proofs through gets annoying
fn inc_three_times {l:addr} (pf: int@l | p: ptr l): (int@l | void) =
let
val (pf2 | ()) = inc_at_ptr (pf | p)
val (pf3 | ()) = inc_at_ptr (pf2 | p)
val (pf4 | ()) = inc_at_ptr (pf3 | p)
in (pf4 | ()) end
// so there's special syntactic sugar for when you don't consume a proof
fn dec_at_ptr {l:addr} (pf: !int@l | p: ptr l): void =
!p := !p - 1 // ^ note the exclamation point
fn dec_three_times {l:addr} (pf: !int@l | p: ptr l): void =
let
val () = dec_at_ptr (pf | p)
val () = dec_at_ptr (pf | p)
val () = dec_at_ptr (pf | p)
in () end
// dataview is like dataprop, but linear
// A proof that either the address is null, or there is a value there
dataview MaybeNull(a:t@ype, addr) =
| NullPtr(a, null)
| {l:addr | l > null} NonNullPtr(a, l) of (a @ l)
fn maybe_inc {l:addr} (pf: !MaybeNull(int, l) | p: ptr l): void =
if ptr1_is_null p
then ()
else let
// Deconstruct the proof to access the proof of a @ l
prval NonNullPtr(value_exists) = pf
val () = !p := !p + 1
// Reconstruct it again for the caller
prval () = pf := NonNullPtr(value_exists)
in () end
// array_v(a,l,n) represents and array of n a's at location l
// this gets compiled into an efficient for loop, since all proofs are erased
fn sum_array {l:addr}{n:nat} (pf: !array_v(int,l,n) | p: ptr l, n: int n): int =
let
fun loop {l:addr}{n:nat} .<n>. (
pf: !array_v(int,l,n)
| ptr: ptr l,
length: int n,
acc: int
): int = if length = 0
then acc
else let
prval (head, rest) = array_v_uncons(pf)
val result = loop(rest | ptr_add<int>(ptr, 1), length - 1, acc + !ptr)
prval () = pf := array_v_cons(head, rest)
in result end
in loop (pf | p, n, 0) end
// 'var' is used to create stack-allocated (lvalue) variables
val seven: int = let
var res: int = 3
// they can be modified
val () = res := res + 1
// addr@ res is a pointer to it, and view@ res is the associated proof
val (pf | ()) = inc_three_times(view@ res | addr@ res)
// need to give back the view before the variable goes out of scope
prval () = view@ res := pf
in res end
// References let you pass lvalues, like in C++
fn square (x: &int): void =
x := x * x // they can be modified
val sixteen: int = let
var res: int = 4
val () = square res
in res end
fn inc_at_ref (x: &int): void =
let
// like vars, references have views and addresses
val (pf | ()) = inc_at_ptr(view@ x | addr@ x)
prval () = view@ x := pf
in () end
// Like ! for views, & references are only legal as argument types
// fn bad (x: &int): &int = x // doesn't compile
// this takes a proof int n @ l, but returns a proof int (n+1) @ l
// since they're different types, we can't use !int @ l like before
fn refined_inc_at_ptr {n:int}{l:addr} (
pf: int n @ l | p: ptr l
): (int (n+1) @ l | void) =
let
val () = !p := !p + 1
in (pf | ()) end
// special syntactic sugar for returning a proof at a different type
fn refined_dec_at_ptr {n:int}{l:addr} (
pf: !int n @ l >> int (n-1) @ l | p: ptr l
): void =
!p := !p - 1
// legal but very bad code
prfn swap_proofs {v1,v2:view} (a: !v1 >> v2, b: !v2 >> v1): void =
let
prval tmp = a
prval () = a := b
prval () = b := tmp
in () end
// also works with references
fn refined_square {n:int} (x: &int n >> int (n*n)): void =
x := x * x
fn replace {a,b:vtype} (dest: &a >> b, src: b): a =
let
val old = dest
val () = dest := src
in old end
// values can be uninitialized
fn {a:vt@ype} write (place: &a? >> a, value: a): void =
place := value
val forty: int = let
var res: int
val () = write (res, 40)
in res end
// viewtype: a view and a type
viewtypedef MaybeNullPtr(a:t@ype) = [l:addr] (MaybeNull(a, l) | ptr l)
// MaybeNullPtr has type 'viewtype' (aka 'vtype')
// type is a subtype of vtype and t@ype is a subtype of vt@ype
// The most general identity function:
fn {a:vt@ype} id7 (x: a) = x
// since they contain views, viewtypes must be used linearly
// fn {a:vt@ype} duplicate (x: a) = (x, x) // doesn't compile
// fn {a:vt@ype} ignore (x: a) = () // doesn't compile
// arrayptr(a,l,n) is a convenient built-in viewtype
fn easier_sum_array {l:addr}{n:nat} (p: !arrayptr(int,l,n), n: int n): int =
let
fun loop {i:nat | i <= n} (
p: !arrayptr(int,l,n), n: int n, i: int i, acc: int
): int =
if i = n
then acc
else loop(p, n, i+1, acc + p[i])
in loop(p, n, 0, 0) end
/*************** Part 5: dataviewtypes ****************/
// a dataviewtype is a heap-allocated non-shared inductive type
// in the stdlib:
// dataviewtype list_vt(a:vt@ype, int) =
// | list_vt_nil(a, 0)
// | {n:nat} list_vt_cons(a, n+1) of (a, list_vt(a, n))
fn {a:vt@ype} length {n:int} (l: !list_vt(a, n)): int n =
let // ^ since we're not consuming it
fun loop {acc:int} (l: !list_vt(a, n-acc), acc: int acc): int n =
case l of
| list_vt_nil() => acc
| list_vt_cons(head, tail) => loop(tail, acc + 1)
in loop (l, 0) end
// vvvvv not vt@ype, because you can't easily get rid of a vt@ype
fun {a:t@ype} destroy_list {n:nat} (l: list_vt(a,n)): void =
case l of
// ~ pattern match consumes and frees that node
| ~list_vt_nil() => ()
| ~list_vt_cons(_, tail) => destroy_list tail
// unlike a datatype, a dataviewtype can be modified:
fun {a:vt@ype} push_back {n:nat} (
x: a,
l: &list_vt(a,n) >> list_vt(a,n+1)
): void =
case l of
| ~list_vt_nil() => l := list_vt_cons(x, list_vt_nil)
// @ pattern match disassembles/"unfolds" the datavtype's view, so you can
// modify its components
| @list_vt_cons(head, tail) => let
val () = push_back (x, tail)
// reassemble it with fold@
prval () = fold@ l
in () end
fun {a:vt@ype} pop_last {n:pos} (l: &list_vt(a,n) >> list_vt(a,n-1)): a =
let
val+ @list_vt_cons(head, tail) = l
in case tail of
| list_vt_cons _ => let
val res = pop_last tail
prval () = fold@ l
in res end
| ~list_vt_nil() => let
val head = head
// Deallocate empty datavtype nodes with free@
val () = free@{..}{0} l
val () = l := list_vt_nil()
in head end
/** Equivalently:
* | ~list_vt_nil() => let
* prval () = fold@ l
* val+ ~list_vt_cons(head, ~list_vt_nil()) = l
* val () = l := list_vt_nil()
* in head end
*/
end
// "holes" (ie uninitialized memory) can be created with _ on the RHS
// This function uses destination-passing-style to copy the list in a single
// tail-recursive pass.
fn {a:t@ype} copy_list {n:nat} (l: !list_vt(a, n)): list_vt(a, n) =
let
var res: ptr
fun loop {k:nat} (l: !list_vt(a, k), hole: &ptr? >> list_vt(a, k)): void =
case l of
| list_vt_nil() => hole := list_vt_nil
| list_vt_cons(first, rest) => let
val () = hole := list_vt_cons{..}{k-1}(first, _)
// ^ on RHS: a hole
val+list_vt_cons(_, new_hole) = hole
// ^ on LHS: wildcard pattern (not a hole)
val () = loop (rest, new_hole)
prval () = fold@ hole
in () end
val () = loop (l, res)
in res end
// Reverse a linked-list *in place* -- no allocations or frees
fn {a:vt@ype} in_place_reverse {n:nat} (l: list_vt(a, n)): list_vt(a, n) =
let
fun loop {k:nat} (l: list_vt(a, n-k), acc: list_vt(a, k)): list_vt(a, n) =
case l of
| ~list_vt_nil() => acc
| @list_vt_cons(x, tail) => let
val rest = replace(tail, acc)
// the node 'l' is now part of acc instead of the original list
prval () = fold@ l
in loop (rest, l) end
in loop (l, list_vt_nil) end
/*************** Part 6: miscellaneous extras ****************/
// a record
// Point has type 't@ype'
typedef Point = @{ x= int, y= int }
val origin: Point = @{ x= 0, y= 0 }
// tuples and records are normally unboxed, but there are boxed variants
// BoxedPoint has type 'type'
typedef BoxedPoint = '{ x= int, y= int }
val boxed_pair: '(int,int) = '(5, 3)
// When passing a pair as the single argument to a function, it needs to be
// written @(a,b) to avoid ambiguity with multi-argument functions
val six_plus_seven = let
fun sum_of_pair (pair: (int,int)) = pair.0 + pair.1
in sum_of_pair @(6, 7) end
// When a constructor has no associated data, such as None(), the parentheses
// are optional in expressions. However, they are mandatory in patterns
fn inc_option (opt: Option int) =
case opt of
| Some(x) => Some(x+1)
| None() => None
// ATS has a simple FFI, since it compiles to C and (mostly) uses the C ABI
%{
// Inline C code
int scanf_wrapper(void *format, void *value) {
return scanf((char *) format, (int *) value);
}
%}
// If you wanted to, you could define a custom dataviewtype more accurately
// describing the result of scanf
extern fn scanf (format: string, value: &int): int = "scanf_wrapper"
fn get_input_number (): Option int =
let
var x: int = 0
in
if scanf("%d\n", x) = 1
then Some(x)
else None
end
// extern is also used for separate declarations and definitions
extern fn say_hi (): void
// later on, or in another file:
implement say_hi () = print "hi\n"
// if you implement main0, it will run as the main function
// implmnt is an alias for implement
implmnt main0 () = ()
// as well as for axioms:
extern praxi view_id {a:view} (x: a): a
// you don't need to actually implement the axioms, but you could
primplmnt view_id x = x
// primplmnt is an alias for primplement
// Some standard aliases are:
// List0(a) = [n:nat] list(a,n) and List0_vt(a) = [n:nat] list_vt(a,n)
// t0p = t@ype and vt0p = vt@ype
fun {a:t0p} append (xs: List0 a, ys: List0 a): List0 a =
case xs of
| list_nil() => ys
| list_cons(x, xs) => list_cons(x, append(xs, ys))
// there are many ways of doing things after one another
val let_in_example = let
val () = print "thing one\n"
val () = print "thing two\n"
in () end
val parens_example = (print "thing one\n"; print "thing two\n")
val begin_end_example = begin
print "thing one\n";
print "thing two\n"; // optional trailing semicolon
end
// and many ways to use local variables
fun times_four_let x =
let
fun times_two (x: int) = x * 2
in times_two (times_two x) end
local
fun times_two (x: int) = x * 2
in
fun times_four_local x = times_two (times_two x)
end
fun times_four_where x = times_two (times_two x)
where {
fun times_two (x: int) = x * 2
}
//// The last kind of comment in ATS is an end-of-file comment.
Anything between the four slashes and the end of the file is ignored.
Have fun with ATS!This isn't all there is to ATS -- notably, some core features like closures and the effect system are left out, as well as other less type-y stuff like modules and the build system. If you'd like to write these sections yourself, contributions would be welcome!
To learn more about ATS, visit the ATS website, in particular the documentation page.