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/.
1// Include the standard library
2#include "share/atspre_define.hats"
3#include "share/atspre_staload.hats"
4
5// To compile, either use
6// $ patscc -DATS_MEMALLOC_LIBC program.dats -o program
7// or install the ats-acc wrapper https://github.com/sparverius/ats-acc and use
8// $ acc pc program.dats
9
10// C-style line comments
11/* and C-style block comments */
12(* as well as ML-style block comments *)
13
14/*************** Part 1: the ML fragment ****************/
15
16val () = print "Hello, World!\n"
17
18// No currying
19fn add (x: int, y: int) = x + y
20
21// fn vs fun is like the difference between let and let rec in OCaml/F#
22fun fact (n: int): int = if n = 0 then 1 else n * fact (n-1)
23
24// Multi-argument functions need parentheses when you call them; single-argument
25// functions can omit parentheses
26val forty_three = add (fact 4, 19)
27
28// let is like let in SML
29fn sum_and_prod (x: int, y: int): (int, int) =
30 let
31 val sum = x + y
32 val prod = x * y
33 in (sum, prod) end
34
35// 'type' is the type of all heap-allocated, non-linear types
36// Polymorphic parameters go in {} after the function name
37fn id {a:type} (x: a) = x
38
39// ints aren't heap-allocated, so we can't pass them to 'id'
40// val y: int = id 7 // doesn't compile
41
42// 't@ype' is the type of all non-linear potentially unboxed types. It is a
43// supertype of 'type'.
44// Templated parameters go in {} before the function name
45fn {a:t@ype} id2 (x: a) = x
46
47val y: int = id2 7 // works
48
49// can't have polymorphic t@ype parameters
50// fn id3 {a:t@ype} (x: a) = x // doesn't compile
51
52// explicity specifying type parameters:
53fn id4 {a:type} (x: a) = id {a} x // {} for non-template parameters
54fn id5 {a:type} (x: a) = id2<a> x // <> for template parameters
55fn id6 {a:type} (x: a) = id {..} x // {..} to explicitly infer it
56
57// Heap allocated shareable datatypes
58// using datatypes leaks memory
59datatype These (a:t@ype, b:t@ype) = This of a
60 | That of b
61 | These of (a, b)
62
63// Pattern matching using 'case'
64fn {a,b: t@ype} from_these (x: a, y: b, these: These(a,b)): (a, b) =
65 case these of
66 | This(x) => (x, y) // Shadowing of variable names is fine; here, x shadows
67 // the parameter x
68 | That(y) => (x, y)
69 | These(x, y) => (x, y)
70
71// Partial pattern match using 'case-'
72// Will throw an exception if passed This
73fn {a,b:t@ype} unwrap_that (these: These(a,b)): b =
74 case- these of
75 | That(y) => y
76 | These(_, y) => y
77
78
79/*************** Part 2: refinements ****************/
80
81// Parameterize functions by what values they take and return
82fn cool_add {n:int} {m:int} (x: int n, y: int m): int (n+m) = x + y
83
84// list(a, n) is a list of n a's
85fun square_all {n:int} (xs: list(int, n)): list(int, n) =
86 case xs of
87 | list_nil() => list_nil()
88 | list_cons(x, rest) => list_cons(x * x, square_all rest)
89
90fn {a:t@ype} get_first {n:int | n >= 1} (xs: list(a, n)): a =
91 case+ xs of // '+' asks ATS to prove it's total
92 | list_cons(x, _) => x
93
94// Can't run get_first on lists of length 0
95// val x: int = get_first (list_nil()) // doesn't compile
96
97// in the stdlib:
98// sortdef nat = {n:int | n >= 0}
99// sortdef pos = {n:int | n >= 1}
100
101fn {a:t@ype} also_get_first {n:pos} (xs: list(a, n)): a =
102 let
103 val+ list_cons(x, _) = xs // val+ also works
104 in x end
105
106// tail-recursive reverse
107fun {a:t@ype} reverse {n:int} (xs: list(a, n)): list(a, n) =
108 let
109 // local functions can use type variables from their enclosing scope
110 // this one uses both 'a' and 'n'
111 fun rev_helper {i:nat} (xs: list(a, n-i), acc: list(a, i)): list(a, n) =
112 case xs of
113 | list_nil() => acc
114 | list_cons(x, rest) => rev_helper(rest, list_cons(x, acc))
115 in rev_helper(xs, list_nil) end
116
117// ATS has three context-dependent namespaces
118// the two 'int's mean different things in this example, as do the two 'n's
119fn namespace_example {n:int} (n: int n): int n = n
120// ^^^ sort namespace
121// ^ ^^^ ^ ^^^ ^ statics namespace
122// ^^^^^^^^^^^^^^^^^ ^ ^ value namespace
123
124// a termination metric can go in .< >.
125// it must decrease on each recursive call
126// then ATS will prove it doesn't infinitely recurse
127fun terminating_factorial {n:nat} .<n>. (n: int n): int =
128 if n = 0 then 1 else n * terminating_factorial (n-1)
129
130
131/*************** Part 3: the LF fragment ****************/
132
133// ATS supports proving theorems in LF (http://twelf.org/wiki/LF)
134
135// Relations are represented by inductive types
136
137// Proofs that the nth fibonacci number is f
138dataprop Fib(n:int, m:int) =
139 | FibZero(0, 0)
140 | FibOne(1, 1)
141 | {n, f1, f2: int} FibInd(n, f1 + f2) of (Fib(n-1,f1), Fib(n-2,f2))
142
143// Proved-correct fibonacci implementation
144// [A] B is an existential type: "there exists A such that B"
145// (proof | value)
146fun fib {n:nat} .<n>. (n: int n): [f:int] (Fib(n,f) | int f) =
147 if n = 0 then (FibZero | 0) else
148 if n = 1 then (FibOne | 1) else
149 let
150 val (proof1 | val1) = fib (n-1)
151 val (proof2 | val2) = fib (n-2)
152 // the existential type is inferred
153 in (FibInd(proof1, proof2) | val1 + val2) end
154
155// Faster proved-correct fibonacci implementation
156fn fib_tail {n:nat} (n: int n): [f:int] (Fib(n,f) | int f) =
157 let
158 fun loop {i:int | i < n} {f1, f2: int} .<n - i>.
159 (p1: Fib(i,f1), p2: Fib(i+1,f2)
160 | i: int i, f1: int f1, f2: int f2, n: int n
161 ): [f:int] (Fib(n,f) | int f) =
162 if i = n - 1
163 then (p2 | f2)
164 else loop (p2, FibInd(p2,p1) | i+1, f2, f1+f2, n)
165 in if n = 0 then (FibZero | 0) else loop (FibZero, FibOne | 0, 0, 1, n) end
166
167// Proof-level lists of ints, of type 'sort'
168datasort IntList = ILNil of ()
169 | ILCons of (int, IntList)
170
171// ILAppend(x,y,z) iff x ++ y = z
172dataprop ILAppend(IntList, IntList, IntList) =
173 | {y:IntList} AppendNil(ILNil, y, y)
174 | {a:int} {x,y,z: IntList}
175 AppendCons(ILCons(a,x), y, ILCons(a,z)) of ILAppend(x,y,z)
176
177// prfuns/prfns are compile-time functions acting on proofs
178
179// metatheorem: append is total
180prfun append_total {x,y: IntList} .<x>. (): [z:IntList] ILAppend(x,y,z)
181 = scase x of // scase lets you inspect static arguments (only in prfuns)
182 | ILNil() => AppendNil
183 | ILCons(a,rest) => AppendCons(append_total())
184
185
186/*************** Part 4: views ****************/
187
188// views are like props, but linear; ie they must be consumed exactly once
189// prop is a subtype of view
190
191// 'type @ address' is the most basic view
192
193fn {a:t@ype} read_ptr {l:addr} (pf: a@l | p: ptr l): (a@l | a) =
194 let
195 // !p searches for usable proofs that say something is at that address
196 val x = !p
197 in (pf | x) end
198
199// oops, tried to dereference a potentially invalid pointer
200// fn {a:t@ype} bad {l:addr} (p: ptr l): a = !p // doesn't compile
201
202// oops, dropped the proof (leaked the memory)
203// fn {a:t@ype} bad {l:addr} (pf: a@l | p: ptr l): a = !p // doesn't compile
204
205fn inc_at_ptr {l:addr} (pf: int@l | p: ptr l): (int@l | void) =
206 let
207 // !p := value writes value to the location at p
208 // like !p, it implicitly searches for usable proofs that are in scope
209 val () = !p := !p + 1
210 in (pf | ()) end
211
212// threading proofs through gets annoying
213fn inc_three_times {l:addr} (pf: int@l | p: ptr l): (int@l | void) =
214 let
215 val (pf2 | ()) = inc_at_ptr (pf | p)
216 val (pf3 | ()) = inc_at_ptr (pf2 | p)
217 val (pf4 | ()) = inc_at_ptr (pf3 | p)
218 in (pf4 | ()) end
219
220// so there's special syntactic sugar for when you don't consume a proof
221fn dec_at_ptr {l:addr} (pf: !int@l | p: ptr l): void =
222 !p := !p - 1 // ^ note the exclamation point
223
224fn dec_three_times {l:addr} (pf: !int@l | p: ptr l): void =
225 let
226 val () = dec_at_ptr (pf | p)
227 val () = dec_at_ptr (pf | p)
228 val () = dec_at_ptr (pf | p)
229 in () end
230
231// dataview is like dataprop, but linear
232// A proof that either the address is null, or there is a value there
233dataview MaybeNull(a:t@ype, addr) =
234 | NullPtr(a, null)
235 | {l:addr | l > null} NonNullPtr(a, l) of (a @ l)
236
237fn maybe_inc {l:addr} (pf: !MaybeNull(int, l) | p: ptr l): void =
238 if ptr1_is_null p
239 then ()
240 else let
241 // Deconstruct the proof to access the proof of a @ l
242 prval NonNullPtr(value_exists) = pf
243 val () = !p := !p + 1
244 // Reconstruct it again for the caller
245 prval () = pf := NonNullPtr(value_exists)
246 in () end
247
248// array_v(a,l,n) represents and array of n a's at location l
249// this gets compiled into an efficient for loop, since all proofs are erased
250fn sum_array {l:addr}{n:nat} (pf: !array_v(int,l,n) | p: ptr l, n: int n): int =
251 let
252 fun loop {l:addr}{n:nat} .<n>. (
253 pf: !array_v(int,l,n)
254 | ptr: ptr l,
255 length: int n,
256 acc: int
257 ): int = if length = 0
258 then acc
259 else let
260 prval (head, rest) = array_v_uncons(pf)
261 val result = loop(rest | ptr_add<int>(ptr, 1), length - 1, acc + !ptr)
262 prval () = pf := array_v_cons(head, rest)
263 in result end
264 in loop (pf | p, n, 0) end
265
266// 'var' is used to create stack-allocated (lvalue) variables
267val seven: int = let
268 var res: int = 3
269 // they can be modified
270 val () = res := res + 1
271 // addr@ res is a pointer to it, and view@ res is the associated proof
272 val (pf | ()) = inc_three_times(view@ res | addr@ res)
273 // need to give back the view before the variable goes out of scope
274 prval () = view@ res := pf
275 in res end
276
277// References let you pass lvalues, like in C++
278fn square (x: &int): void =
279 x := x * x // they can be modified
280
281val sixteen: int = let
282 var res: int = 4
283 val () = square res
284 in res end
285
286fn inc_at_ref (x: &int): void =
287 let
288 // like vars, references have views and addresses
289 val (pf | ()) = inc_at_ptr(view@ x | addr@ x)
290 prval () = view@ x := pf
291 in () end
292
293// Like ! for views, & references are only legal as argument types
294// fn bad (x: &int): &int = x // doesn't compile
295
296// this takes a proof int n @ l, but returns a proof int (n+1) @ l
297// since they're different types, we can't use !int @ l like before
298fn refined_inc_at_ptr {n:int}{l:addr} (
299 pf: int n @ l | p: ptr l
300): (int (n+1) @ l | void) =
301 let
302 val () = !p := !p + 1
303 in (pf | ()) end
304
305// special syntactic sugar for returning a proof at a different type
306fn refined_dec_at_ptr {n:int}{l:addr} (
307 pf: !int n @ l >> int (n-1) @ l | p: ptr l
308): void =
309 !p := !p - 1
310
311// legal but very bad code
312prfn swap_proofs {v1,v2:view} (a: !v1 >> v2, b: !v2 >> v1): void =
313 let
314 prval tmp = a
315 prval () = a := b
316 prval () = b := tmp
317 in () end
318
319// also works with references
320fn refined_square {n:int} (x: &int n >> int (n*n)): void =
321 x := x * x
322
323fn replace {a,b:vtype} (dest: &a >> b, src: b): a =
324 let
325 val old = dest
326 val () = dest := src
327 in old end
328
329// values can be uninitialized
330fn {a:vt@ype} write (place: &a? >> a, value: a): void =
331 place := value
332
333val forty: int = let
334 var res: int
335 val () = write (res, 40)
336 in res end
337
338// viewtype: a view and a type
339viewtypedef MaybeNullPtr(a:t@ype) = [l:addr] (MaybeNull(a, l) | ptr l)
340// MaybeNullPtr has type 'viewtype' (aka 'vtype')
341// type is a subtype of vtype and t@ype is a subtype of vt@ype
342
343// The most general identity function:
344fn {a:vt@ype} id7 (x: a) = x
345
346// since they contain views, viewtypes must be used linearly
347// fn {a:vt@ype} duplicate (x: a) = (x, x) // doesn't compile
348// fn {a:vt@ype} ignore (x: a) = () // doesn't compile
349
350// arrayptr(a,l,n) is a convenient built-in viewtype
351fn easier_sum_array {l:addr}{n:nat} (p: !arrayptr(int,l,n), n: int n): int =
352 let
353 fun loop {i:nat | i <= n} (
354 p: !arrayptr(int,l,n), n: int n, i: int i, acc: int
355 ): int =
356 if i = n
357 then acc
358 else loop(p, n, i+1, acc + p[i])
359 in loop(p, n, 0, 0) end
360
361
362/*************** Part 5: dataviewtypes ****************/
363
364// a dataviewtype is a heap-allocated non-shared inductive type
365
366// in the stdlib:
367// dataviewtype list_vt(a:vt@ype, int) =
368// | list_vt_nil(a, 0)
369// | {n:nat} list_vt_cons(a, n+1) of (a, list_vt(a, n))
370
371fn {a:vt@ype} length {n:int} (l: !list_vt(a, n)): int n =
372 let // ^ since we're not consuming it
373 fun loop {acc:int} (l: !list_vt(a, n-acc), acc: int acc): int n =
374 case l of
375 | list_vt_nil() => acc
376 | list_vt_cons(head, tail) => loop(tail, acc + 1)
377 in loop (l, 0) end
378
379// vvvvv not vt@ype, because you can't easily get rid of a vt@ype
380fun {a:t@ype} destroy_list {n:nat} (l: list_vt(a,n)): void =
381 case l of
382 // ~ pattern match consumes and frees that node
383 | ~list_vt_nil() => ()
384 | ~list_vt_cons(_, tail) => destroy_list tail
385
386// unlike a datatype, a dataviewtype can be modified:
387fun {a:vt@ype} push_back {n:nat} (
388 x: a,
389 l: &list_vt(a,n) >> list_vt(a,n+1)
390): void =
391 case l of
392 | ~list_vt_nil() => l := list_vt_cons(x, list_vt_nil)
393 // @ pattern match disassembles/"unfolds" the datavtype's view, so you can
394 // modify its components
395 | @list_vt_cons(head, tail) => let
396 val () = push_back (x, tail)
397 // reassemble it with fold@
398 prval () = fold@ l
399 in () end
400
401fun {a:vt@ype} pop_last {n:pos} (l: &list_vt(a,n) >> list_vt(a,n-1)): a =
402 let
403 val+ @list_vt_cons(head, tail) = l
404 in case tail of
405 | list_vt_cons _ => let
406 val res = pop_last tail
407 prval () = fold@ l
408 in res end
409 | ~list_vt_nil() => let
410 val head = head
411 // Deallocate empty datavtype nodes with free@
412 val () = free@{..}{0} l
413 val () = l := list_vt_nil()
414 in head end
415 /** Equivalently:
416 * | ~list_vt_nil() => let
417 * prval () = fold@ l
418 * val+ ~list_vt_cons(head, ~list_vt_nil()) = l
419 * val () = l := list_vt_nil()
420 * in head end
421 */
422 end
423
424// "holes" (ie uninitialized memory) can be created with _ on the RHS
425// This function uses destination-passing-style to copy the list in a single
426// tail-recursive pass.
427fn {a:t@ype} copy_list {n:nat} (l: !list_vt(a, n)): list_vt(a, n) =
428 let
429 var res: ptr
430 fun loop {k:nat} (l: !list_vt(a, k), hole: &ptr? >> list_vt(a, k)): void =
431 case l of
432 | list_vt_nil() => hole := list_vt_nil
433 | list_vt_cons(first, rest) => let
434 val () = hole := list_vt_cons{..}{k-1}(first, _)
435 // ^ on RHS: a hole
436 val+list_vt_cons(_, new_hole) = hole
437 // ^ on LHS: wildcard pattern (not a hole)
438 val () = loop (rest, new_hole)
439 prval () = fold@ hole
440 in () end
441 val () = loop (l, res)
442 in res end
443
444// Reverse a linked-list *in place* -- no allocations or frees
445fn {a:vt@ype} in_place_reverse {n:nat} (l: list_vt(a, n)): list_vt(a, n) =
446 let
447 fun loop {k:nat} (l: list_vt(a, n-k), acc: list_vt(a, k)): list_vt(a, n) =
448 case l of
449 | ~list_vt_nil() => acc
450 | @list_vt_cons(x, tail) => let
451 val rest = replace(tail, acc)
452 // the node 'l' is now part of acc instead of the original list
453 prval () = fold@ l
454 in loop (rest, l) end
455 in loop (l, list_vt_nil) end
456
457
458/*************** Part 6: miscellaneous extras ****************/
459
460// a record
461// Point has type 't@ype'
462typedef Point = @{ x= int, y= int }
463val origin: Point = @{ x= 0, y= 0 }
464
465// tuples and records are normally unboxed, but there are boxed variants
466// BoxedPoint has type 'type'
467typedef BoxedPoint = '{ x= int, y= int }
468val boxed_pair: '(int,int) = '(5, 3)
469
470// When passing a pair as the single argument to a function, it needs to be
471// written @(a,b) to avoid ambiguity with multi-argument functions
472val six_plus_seven = let
473 fun sum_of_pair (pair: (int,int)) = pair.0 + pair.1
474 in sum_of_pair @(6, 7) end
475
476// When a constructor has no associated data, such as None(), the parentheses
477// are optional in expressions. However, they are mandatory in patterns
478fn inc_option (opt: Option int) =
479 case opt of
480 | Some(x) => Some(x+1)
481 | None() => None
482
483// ATS has a simple FFI, since it compiles to C and (mostly) uses the C ABI
484%{
485// Inline C code
486int scanf_wrapper(void *format, void *value) {
487 return scanf((char *) format, (int *) value);
488}
489%}
490// If you wanted to, you could define a custom dataviewtype more accurately
491// describing the result of scanf
492extern fn scanf (format: string, value: &int): int = "scanf_wrapper"
493
494fn get_input_number (): Option int =
495 let
496 var x: int = 0
497 in
498 if scanf("%d\n", x) = 1
499 then Some(x)
500 else None
501 end
502
503// extern is also used for separate declarations and definitions
504extern fn say_hi (): void
505// later on, or in another file:
506implement say_hi () = print "hi\n"
507
508// if you implement main0, it will run as the main function
509// implmnt is an alias for implement
510implmnt main0 () = ()
511
512// as well as for axioms:
513extern praxi view_id {a:view} (x: a): a
514// you don't need to actually implement the axioms, but you could
515primplmnt view_id x = x
516// primplmnt is an alias for primplement
517
518// Some standard aliases are:
519// List0(a) = [n:nat] list(a,n) and List0_vt(a) = [n:nat] list_vt(a,n)
520// t0p = t@ype and vt0p = vt@ype
521fun {a:t0p} append (xs: List0 a, ys: List0 a): List0 a =
522 case xs of
523 | list_nil() => ys
524 | list_cons(x, xs) => list_cons(x, append(xs, ys))
525
526// there are many ways of doing things after one another
527val let_in_example = let
528 val () = print "thing one\n"
529 val () = print "thing two\n"
530 in () end
531
532val parens_example = (print "thing one\n"; print "thing two\n")
533
534val begin_end_example = begin
535 print "thing one\n";
536 print "thing two\n"; // optional trailing semicolon
537 end
538
539// and many ways to use local variables
540fun times_four_let x =
541 let
542 fun times_two (x: int) = x * 2
543 in times_two (times_two x) end
544
545local
546 fun times_two (x: int) = x * 2
547in
548 fun times_four_local x = times_two (times_two x)
549end
550
551fun times_four_where x = times_two (times_two x)
552 where {
553 fun times_two (x: int) = x * 2
554 }
555
556//// The last kind of comment in ATS is an end-of-file comment.
557
558Anything between the four slashes and the end of the file is ignored.
559
560Have 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, in particular the documentation page.