Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In Chapter 1 of Practical Foundations for Programming Languages, the author mentions that abstract syntax trees are associated with sorts.
Intuitively, sorts are like types, but I'd like to know if they have a precise definition. I'd be glad if some references are provided as well.
It depends on what semantics we would take for types and sorts. -- However a brief - little informal - definitions could be - Sorts are classes of ASTs and types are classes of values.
There is actually much similarity between sorts for the abstact syntax and types as usually understood. But sorts are a formal syntactic concept, and AS trees are syntax too, while types are a semantic concept.
The terminology comes from term algebras (also called free algebras) and universal algebra. These are essentially syntactic theories of algebraic structures, analyzed independently of any interpretations. They were developed in the first half of the 20th century.
A term may be seen as a tree, where the nodes are labeled from a finite set of operators, each operator having a fixed arity that specifies the number of daughters in the tree. Arity 0 is for leaves. In multi-sorted algebras this is refined with sorts, so that each operator belong to a sort, and arities are replaced by an ordered list of sorts, that fixes for each daughter the sort of its head operator. The sort of an operator, together with the list of the sorts of its daughter, is called the signature of the operator.
In universal algebras, this is further refined by introducing equationally defined equivalence relations between terms.
Though it seems to have faded a bit, these concepts were quite popular and much studied in computer science in the late 20th century, as abstract algebras where then seen as a basis for abstract data types, which is, in part, precursor of what is nos classes in object oriented programming.
Universal algebras are related to the development of category theory, which is also foundational in current vision of types and programming languages.
Algebras are syntactic object, and are intended to be used with an interpretation in some semantic domain(s) corresponding to types. An interpretation is a homomorphism that maps sorts into domains of values (types), and operators into functions between those domains, so that signatures are respected, and equations too in the case of an equational algebra. This is how you can apply the results of group theory to any domain with an operation that respect the definition of a group.
This organization was considered very convenient by early researchers in programming languages, especially those concerned with formalizing programming languages. It had the advantage of isolating syntax and semantics, and of being mathematically well understood.
Another reason for adopting it was a concern with the development of tool to manipulate programs, either in development environments or in formal systems to prove properties of programs (which turned out to be more and more twin problems).
This lead to the emergence of the concept of abstract syntax tree (AST) for programming languages, which are essentially terms of a multi-sorted algebra (sometimes refined with a use of sort union in some sytems). The AST is the reference syntax for a language, from which semantics can be defined by homomorphism as in denotational semantics.
Not only is this convenient to study semantics of languages, but trees are better structured thans strings and thus a better basis for developing programming tools and programming environments.
It allows to isolate parsing which was traditionnally a messy part as the limitations of parsing technology forced the use of distorted grammars. It also factors out presentation issues.
It allows for multiple concrete (string or graphic) representations of programs, which can sometimes be convenient (there is no reason why using punctuation rather than tabs, or the converse, in program syntax should be forced on people).
It makes it easy to define many interpretations of programs, and of sorts, in order to analyze program properies with abstract interpretations.
It is convenient for writing (semi-)automated program manipulation tools, for example for automatic program transformations, or translations between languages.
Things may sometimes be a bit more complicated in practice, because some forms of Abstract Syntax allow some operators to buid trees (expressions) that belong to several sorts (an informal way to look at it). For example there could be a sort for syntactic constructs that represent variables (assignable entities), and another for expressions. But any variable can be used as an expression, the converse being false.
Early papers on this, for programming languages, date back to the mid-seventies. The conceptualization at the time was intended for the production of syntax conscious (the word "directed" was then used) programming environments. Look for Mentor and Centaur in Europe and for Cornell Program Synthesizer in the USA. They were the first two system to actually use such concepts in a practical way. Many others were developped afterwards.
But abstract syntax predates these systems. The Lisp language (1958) had abstract syntax, which is no surprise as it was developed by a logician, and for the purpose of making programs that manipulate programs (see also ML and LCF ... that came later). But Lisp was not sorted : everything was syntactically a list and more refined structure was essentially semantics dependent. This lead some people to consider, somewhat incorrectly, that Lisp had no syntax.
It appears in chapter four that sorts are for syntax and types are for semantics.
The example syntax chart on page 40 deals with the sorts in the language L{num str}. Apparently sorts are categories in the syntax of the language.
In particular, "plus" has a sort, which is the syntactic category of its result. The sort of the operator "plus" is named "Exp". That represents the fact that syntactically, an invocation of the operator "plus" is an expression. An invocation of the operator "plus" can fill a position in an abstract syntax tree where an expression is permitted. That's what kind of construction a "plus" is. That's how it fits into the structure of a text that represents a program.
The type system on page 41 deals with the types in language L{num str}. The type of operator "plus", given that its operands have type "num", is "num". This judgment is a partial description of the semantics of operator "plus". That is, part of the meaning of the operator "plus" is the combining of two numbers to produce a number. This meaning distinguishes "plus" from other expressions.
Furthermore, there is a sort named "Typ" that contains the two types, "num" and "str".
In the beginning of Chapter 1, Harper gives a hint as to what he means by the word sort:
The syntax of a language specifies the means by which various sorts of phrases (expressions, commands, declarations, and so forth) may be combined to form programs.
He defines the word phrase as an abstract syntax tree, which he then discusses.
