Add documentation for ATS (#4089)

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).
+