Style guide

Functional Programming (FP) style in ATS.

There is no style that is considered official*, though one can take a look at existing ATS library sources to get a sense of one good style

(Insert sagely advice in this paragraph) As with many things, optimal learning can be achieved by different people in different ways. A suggestion for functional programming in general, to those who have experience in imperative programming, is to read examples, understand examples, and implement examples. Much like math or writing literature, most people need practice and experience to really become effective. Abstraction is an important mechanism in making good style (and good code) possible. This code example for a calculator, while not exactly a tutorial, demonstrates these principles. Discussion on the calculator example is located here.

(Any good journals or sites accessible to a beginner that aren't ATS specific but still applicable for an ATS beginner?)

There are many examples in the ATS2 Book, and also some examples listed separately.

Some examples of poor versus good implementations in ATS:

A simple tokenizer.

How NOT to use references.

Using case with conditionals. An alternative to using a string of if-then-else expressions is to use a case-when expression. This is more powerful and elegant than if-then-else because pattern matching can also be integrated, and the syntax is more compact. For a simple example emulating switch-case without pattern matching, see the following:

(*
We are testing x for several possible values.
We use case+ of 0, but we could use "of anything"
since the anything doesn't matter in this case.
*)
case+ 0 of
| _ when x = 1 || x = 3 => print("An odd int < 5\n")
| _ when x = 2 || x = 4 => print("An even int < 5\n")
| _ => print("Not 1, 2, 3, or 4.\n")

val vs var Some very good material on how to deal with val and var bindings, which come from functional and imperative programming respectively, can be found on the old ATS site.

Additionally, some static assignment features supported by val are currently unsupported by var, but in principle could be added. As a work around, intermediate vals can be used.

Loops

Examples abound on using tail-recursive functions as loops in place of while and for loops to achieve the same effect in a functional programming style. Often, it is useful to declare a function as being <cloref> to allow the function to use variables defined outside of its body or argument list; <cloref> means "the function is a peristent closure that requires the garbage collector to be freed". Apparently, this does not mean that a closure is actually created each time a <cloref> function is called, as it is heap allocated. See this tutorial for further details.

Style with dependent types.

Dependent types are often difficult to use, and should be avoided when possible on the first pass of writing an implementation. Their use can overly complicate program implementation by a very large margin; so a non-dependent "program-first program verification" approach, possibly with linear types, is encouraged.

An example of this is a sort for doubles and floats, which no longer exists in ATS due to its propensity for complicating code.

The same caution and program-first program verification approach can likely be applied to writing proof functions in ATS.

Style with linear types.

Linear types are generally easy to use, with a few exceptions, such as dataviewtypes. No knowledge of linear logic formalisms is necessary for using linear types in ATS. Perhaps the main issue for beginners with linear types, or at least linear types in ATS, will be getting used to a somewhat large body of syntactical features; many of these share some overlap in their conceptual usage but operate on different resources. This is somewhat in contrast to dependent types, where the syntax is relatively easy, but keeping track of the logic in one's mind can become quite a burden. This makes using dependent type all too easy to get one in to trouble with the typechecker (see above).

An example of using linear types with unlimited precision integers (using GMP) is available, which should be useful for beginners to learn linear types.

Naming conventions (for types and others)

• For a type named g0xxxx, g stands generic and 0 for un-indexed, See: Naming convention, on ats-lang-users
• For a type named g1xxxx, g stands generic and 1 for indexed, See: Naming convention, on ats-lang-users
• Many type names, like eg. size_t, reuse that of C
• A type named xxxx_vt is typical for a view‑type
• A function should be given a name indicating it is a loop, like loop or foo_loop, only if it is tail‑recursive; see Recursively Defined Datatypes, in Intro to ATS
• With functional relations à la Prolog, the result is the last element, and the arguments are the first elements ; ex. while one may write val r = fib(n); with the result on the left, one would better write FIB(n, r), with the result on the right, to express the relationship