summaryrefslogtreecommitdiffhomepage
path: root/ATS.html.markdown
diff options
context:
space:
mode:
Diffstat (limited to 'ATS.html.markdown')
-rw-r--r--ATS.html.markdown607
1 files changed, 607 insertions, 0 deletions
diff --git a/ATS.html.markdown b/ATS.html.markdown
new file mode 100644
index 00000000..f290ac0f
--- /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/).
+
+
+```ocaml
+// 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).
+