I'm interested in the relative merits of ATS vs. Epigram which is a Pure Type System that seeks to unify types and terms, where ATS distinguishes the statics and dynamics of the language. What benefits and limitations do these approaches have on complexity for both developer and implementor? notes in atsVepig.txt
ATS is a PL with a highly expressive type system from the framework Applied Type System. Both dependent types and linear types are available in ATS. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ and supports * Functional programming. ATS uses eager call-by-value eval, it also supports lazy call-by-need evaluation. Linear types in ATS can often make FP run with high efficiency * Imperative programming. While features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory mgmt) are allowed in ATS, the type system of ATS is still able to guarantee that no run-time errors can occur * Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads and parallel let * Modular programming. The module system of ATS is largely infuenced by that of Modula-3
Some Basics on ATS ATS consists of a static component (statics), where types are formed and reasoned about, and a dynamic component (dynamics), where programs are constructed and evaluated. Some Primitive Sorts and Constants The statics of ATS is a simply typed language. The types for terms in the statics are called sorts (so as to avoid potential confusion with the types for terms in the dynamics) and the terms in it are called static terms. We use sigma for sorts and s for static term. The primitive sorts in ATS include bool, int, prop, type, view and viewtype. There are also some primitive constants c in the statics, each of which is assigned a constant sort (or c-sort, for short) of the following form:
ATS is a functional language that supports a variety of advanced types such as dependent types and linear types, and Anairiats is the current implementation of ATS. ATS/Anairiats can run with or without (systematic) garbage collection (GC), and its performance is comparable to imperative languages like C and C++. # File Inclusion # Compilation # The Main Function in ATS # Fixity Declaration # Overloading # Function or Closure? # Variadic Functions # Tail-Recursive Functions # Termination Metrics # Types with Effects # Call-By-Reference # (Persistent) Lists # Linear Lists # Pointers # References # (Persistent) Arrays and Matrices # Linear Arrays # Datatypes # Dataprops # Dataviews # Dataviewtypes # Pattern Matching # Exceptions # Val(ue) and Var(iable) Declarations # Higher-Order Functions # Lazy Evaluation # Macros # Templates # Memory Allocation/Deallocation # Input and Output # Combining ATS and C programs # Programming with Theorem Proving