This is an interesting talk given by my adviser Prof. Xi. And I will try my best to put the ideas here in a proper way.
Type Systems in a Word
Type systems are systems about types. They have basic types, complex types, and the rules to construct complex types using basic types. There are also other essential theories in a type system, like how to decide the type of a term by using some rules. ATS, as its name (Applied Type System) indicates, is a type system. It has its own basic types, its rules of describe complex types, and many related theories.
There are different kinds of type systems. Some use basic types to describe complex types, and use complex types to describe even more complex types. That's something that has a hierarchical structure. We could say that they are hierarchical type systems. Other type systems may not have a hierarchy. They involves something like cyclic definitions, like Martin-Lof's Type Theory. ATS chose to be a hierarchical type system. (But, my adviser expressed his thoughts that cyclic defined systems may be more advanced in some aspects, especially in math.)
In ATS, there is a base level of types, and two more levels of types upon that base. They are sorts, statics, and dynamics respectively. Sorts are basic types that describe or construct statics. And statics are used to constructs more complex types which are going to be used in dynamics.
Before statics, let's talk about sorts, which is the base level of types. In ATS paper, sorts are defined as
\[\sigma := b \mid \sigma\_1 \rightarrow \sigma\_2\]
The \(b\) stands for basic sorts, which are sorts that can't be simpler, like
t@ype. And \(\sigma\_1 \rightarrow \sigma\_2\) is also defined to be sort. They can be regarded as the sort for functions. But in real ATS statics, it hasn't been supported yet, because there is actually no real lambda abstractions and function applications. These sorts will be further used to describe (construct) static terms. Terms refer to lambda terms, and they may be covered in the following blogs. From my understanding, terms are the core part of statics and dynamics, and any other programming languages. It represents those constructive components in a programming language, like variables, statements, functions and function calls, and so on. In a typed language (I am not sure, but at least ATS), each term will be assigned a type. Specifically, each static term will be assigned a sort using some rules. This is what I mean by saying "use sorts to describe or construct static terms".
Statics could be regarded as a language to describe complex static terms. The syntax is well-defined in the paper, and the first syntax is the sort syntax shown above. The rests are
static terms: ~ \(s := a \mid \lambda a : \sigma.s \mid s\_1(s\_2) \mid sc(s\_1,s\_2,\cdots,s\_n)\)
static variable context: ~ \(\Sigma := \emptyset \mid \Sigma,a:\sigma\)
signatures: ~ \(S := S\_\emptyset \mid S, sc:[\sigma\_1,\cdots,\sigma\_n] \Rightarrow b\)
static substitution: ~ \(\Theta\_S := |\Theta\_S [a \mapsto s]\)
The static terms are quite similar to lambda terms in typed lambda calculus. \(a\) is variable. \(\lambda a: \sigma.s\) is lambda abstraction, which stands for functions. \(s\_1(s\_2)\) is function application, or function call. The only difference is \(sc(s\_1,\cdots,s\_n)\). It is a special kind of function applications, which apply static constants \(sc\) to static terms \(s\_1,\cdots,s\_n\).
Static constants include static constant constructors like
int(n), and static constant functions like
+ operator. Or you can just call them static constant functions, because they are essentially the same. Although they could both be classified as lambda abstractions or functions (or more precisely, predefined functions in ATS), ATS does so because of some practical implementation considerations. If you try to encode the plus operator using pure typed lambda calculus, that could be a lot of work. So ATS just extract them into a separate definition. I don't know too much about it currently, but I may explain it later when I learn more. Come back to static constants. Their definitions are described in \(signatures\). The first part \(S\_\emptyset\) contains some predefined basic definitions. And the second part is an expansion rule which expands \(S\) to include a new signature \(sc\) of the "sort" \((\sigma\_1,\cdots,\sigma\_n)\Rightarrow b\). In order to avoid the conflict between the sort for static constants, and the sort defined previously, ATS calls "sc-sort" for the sort of static constants. (There ARE lambda abstractions and function applications in ATS statics. You can define a sort in the form of \(\sigma\_1 \rightarrow \sigma\_2\). And you can apply it, too.) If you would like to gain some real feel, skip to the end for examples.
Dynamics are all about proofs and programs. In a word, you use dynamics to construct a real program, while you use statics to describe dynamics, or to write specifications of dynamics. Proofs are also programs, but they produce propositions to prove something. Dynamics are very similar to statics. Dynamic terms will be assigned types. Those types are static terms of sort
type(or t@ype). There is also a formal definition for dynamic terms, dynamic values, variable context, and substitution. But it is too complex for me now. I will cover that later on. Not that there is a "dynamic values". As far as I know, they are dynamic terms that couldn't be further simplified, like a termination token in a programming language grammar.
datasort mylist = | nil of () | cons of (int, mylist) stadef list = cons (1, nil())
In this statics example, we defined a sort called
mylist, which is part of the base sort \(\sigma := b\) in the paper. The
consis a static constant of
sc-sort \((int, mylist) \Rightarrow mylist\). The
cons (1, nil()) are static constant applications, which are defined to be static terms, of sort
listis a static term, of sort
mylist. Note that, the static constant should be of form \([\sigma\_1,\cdots,\sigma\_n] \Rightarrow b\) instead of \([\sigma\_1,\cdots,\sigma\_n] \Rightarrow \sigma\_p \rightarrow \sigma\_q\).
fun myplus (a:int, b:int): int
In this dynamics example, we defined a function
myplus, which is a dynamic term, of type \((int, int) \rightarrow int\). The type \((int, int) \rightarrow int\) is a static term of sort
type. This static term is of the form of static constant application with the static constant being the \(\rightarrow\) symbol. It is a static constant who takes static terms (of sort
type) and produces static terms (of sort
type). The \(\rightarrow\) is defined as a member of \(S\_\emptyset\) in the statics syntax. Please refer to the paper.
ATS paper could be found here