http://www.ats-lang.org/ The ATS Programming Language Unleashing the Potentials of Types and Templates! * Home What is ATS? What is ATS good for? Suggestion on learning ATS Acknowledgments * Downloads ATS packages Uninstallation for ATS Requirements for installation Precompiled packages for installation Installation through source compilation Installation of ATS2-contrib Installation of ATS2-include Scripts for installing ATS-Postiats * Documents [ ] Introduction to Programming in ATS A Tutorial on Programming Features in ATS A Crash into Functional Programming via ATS Effective Programming in ATS through Examples * Libraries * Community Wiki for ATS users ATS news links at reddit IRC channel for ATS users StackOverflow tag for ATS Q&A forum for ATS users Discussion forum for ATS developers Mailing-list for ATS users JATS-UG: Japan ATS User Group About ATS * What is ATS? * What is ATS good for? * Suggestion on learning ATS * Acknowledgments -------------------- What is ATS? ATS is a statically typed programming language that unifies implementation with formal specification. It is equipped with a highly expressive type system rooted in the framework Applied Type System, which gives the language its name. In particular, both dependent types and linear types are available in ATS. The current implementation of ATS2 (ATS/Postiats) is written in ATS1 (ATS/Anairiats), consisting of more than 180K lines of code. ATS can be as efficient as C/C++ both time-wise and memory-wise and supports a variety of programming paradigms that include: * Functional programming. The core of ATS is a call-by-value functional language inspired by ML. The availability of linear types in ATS often makes functional programs written in it run not only with surprisingly high efficiency (when compared to C) but also with surprisingly small (memory) footprint (when compared to C as well). * Imperative programming. The novel approach to imperative programming in ATS is firmly rooted in the paradigm of programming with theorem-proving. The type system of ATS allows many features considered dangerous in other languages (such as explicit pointer arithmetic and explicit memory Yes, ATS can! allocation/ deallocation) to ---------------------------------------- be safely supported in What is new in the community? GO ATS, making ATS well-suited for ---------------------------------------- implementing high-quality Would you like to try ATS on-line? OK low-level systems. ---------------------------------------- * Concurrent programming. ATS The core of ATS is a typed call-by-value can support functional programming language that is multithreaded largely inspired by ML. For instance, programming the following tiny ATS program is through safe use written in a style of functional of pthreads. The programming: availability of linear types for [// ] tracking and [// Yes, you can edit ] safely [// ] manipulating [(* Say Hello! once *) ] resources [val () = print"Hello!\n" ] provides an [// ] effective [(* Say Hello! 3 times *) ] ATSlogo approach to [val () = 3*delay(print"Hello!") ] Home(old) constructing [val () = print_newline((*void*)) ] Downloads reliable [// ] Documents programs that Try-it-yourself Libraries can take great Community advantage of ---------------------------------------- Papers multicore Examples architectures. ATS is both accurate and expressive in Resources * Modular its support for (static) typechecking. Implements programming. The The following code demonstrates the Mailing-list module system of ability of ATS in detecting ats-lang-users ATS is largely out-of-bounds subscripting at ats-lang-devel infuenced by compile-time: Try ATS that of on-line Modula-3, which [// ] is both simple [// Yes, you can edit ] and general as [// ] well as [(* Build a list of 3 *) ] effective in [val xs = $list{int}(0, 1, 2) ] supporting large [// ] scale [val x0 = xs[0] // legal ] programming. [val x1 = xs[1] // legal ] [val x2 = xs[2] // legal ] In addition, ATS [val x3 = xs[3] // illegal ] contains a subsystem [// ] ATS/LF that supports Try-it-yourself a form of (interactive) ---------------------------------------- theorem-proving, where proofs are ATS is highly effective and flexible in constructed as total its support for a template-based functions. With this approach to code reuse. As an example, subsystem, ATS is the following code is likely to remind able to advocate a someone of higher-order functions but it programmer-centric is actually every bit of a first-order approach to program implementation in ATS: verification that combines programming [// ] with theorem-proving [// Yes, you can edit ] in a syntactically [// ] intertwined manner. [extern ] Furthermore, ATS/LF [fun{} f0 (): int ] can also serve as a [extern ] logical framework [fun{} f1 (int): int ] (LF) for encoding [extern ] various formal [fun{} repeat_f0f1 (int): int ] systems (such as [// ] logic systems and [implement ] type systems) [{}(*tmp*) ] together with proofs Try-it-yourself of their (meta-) properties. ---------------------------------------- -------------------- With a functional core of ML-style and certain ad-hoc support for overloading What is ATS good (of function symbols), ATS can readily for? accommodate a typical combinator-based style of coding that is often considered * ATS can greatly a prominent signature of functional enforce programming. The following "one-liner" precision in solution to the famous Queen Puzzle practical should offer a glimpse of using programming. combinators in ATS: * ATS can greatly facilitate [// ] refinement-based [(* Solving the Queen Puzzle *) ] software [// ] development. [#define N 8 // it can be changed ] * ATS allows the [#define NSOL 10 // it can be changed] programmer to [// ] write efficient [val () = ] functional [(((fix qsolve(n: int): stream(list0(] programs that [// ] directly [ ] manipulate Try-it-yourself native unboxed data Please find on-line the entirety of this representation. example, which is meant to showcase * ATS allows the programming with combinators in ATS. programmer to reduce the ---------------------------------------- memory footprint of a program by making use of linear types. * ATS allows the programmer to enhance the safety (and efficiency) of a program by making use of theorem-proving. * ATS allows the programmer to write safe low-level code that runs in OS kernels. * ATS can help teach type theory, demonstrating both convincingly and concretely the power and potential of types in constructing high-quality software. -------------------- Suggestion on learning ATS ATS is feature-rich (like C++). Prior knowledge of functional programming based on ML and imperative programming based on C can be a big plus for learning ATS. In general, one should expect to encounter many unfamiliar programming concepts and features in ATS and be prepared to spend a substantial amount of time on learning them. Hopefully, one will become a superbly confident programmer at the end who can enjoy implementing large and complex systems with minimal need for debugging. -------------------- Acknowledgments The development of ATS has been funded in part by National Science Foundation (NSF) under the grants no. CCR-0081316/ CCR-0224244, no. CCR-0092703/0229480, no. CNS-0202067, no. CCF-0702665 and no CCF-1018601. As always, any opinions, findings, and conclusions or recommendations expressed here are those of the author (s) and do not necessarily reflect the views of the NSF. -------------------- [thePageRFooterSep] This page is created by Hongwei Xi with tools including ATS/weboxy, atscc2js and atscc2php.