diff options
| -rw-r--r-- | ATS.html.markdown | 607 |
1 files changed, 607 insertions, 0 deletions
diff --git a/ATS.html.markdown b/ATS.html.markdown new file mode 100644 index 00000000..0ec785a5 --- /dev/null +++ b/ATS.html.markdown @@ -0,0 +1,607 @@ +--- +language: ATS +contributors: + - ["Mark Barbone", "https://github.com/mb64"] +filename: 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](http://twelf.org/wiki/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](http://www.ats-lang.org/SERVER/MYCODE/Patsoptaas_serve.php), +or install it from [http://www.ats-lang.org/](http://www.ats-lang.org/). + + +```ats +// 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! +``` + +## Learn more + +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](http://www.ats-lang.org/), in +particular the [documentation page](http://www.ats-lang.org/Documents.html). + |