9
$\begingroup$

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.

$\endgroup$

migrated from cstheory.stackexchange.com May 2 '13 at 14:41

This question came from our site for theoretical computer scientists and researchers in related fields.

4
$\begingroup$

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.

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Would you say there are 2 different hierarchies, one in the syntax land, and another in semantics land. In syntax we have as you ASTs and sorts and classes of sorts. In semantics we have values, types, kinds... etc. Aren't there languages that unify both into one development environment like Twelf or Coq? $\endgroup$ – CMCDragonkai Feb 2 '16 at 4:43
  • $\begingroup$ @CMCDragonkai I would say (barring possible mistakes) precisely what I said. I would not call these hierarchies, but rather domains of (meta-)discourse. The syntax-semantics separation distinguishes what we talk about and how we do it, which requires representation. You should not want to mix syntax and semantics of the same language, but syntax of one language can be an object of discourse, hence belong to the semantics of another language. In that sense you might see some unification, to be handled with care. Syntax is always finitely generated, while semantics has no such constraint. $\endgroup$ – babou Feb 2 '16 at 11:06
2
$\begingroup$

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".

$\endgroup$
  • 1
    $\begingroup$ Well, he uses it in this concept, but he doesn't define it clearly. I found the term "Many-sorted logic" which seems to me that sorts and types are really closed related concepts. I just wanted to know a clear definition for both. $\endgroup$ – rslima May 6 '13 at 11:10
  • $\begingroup$ It's something to do with "pure type systems". I suspect we could consider the presentation in "Lambda Calculi with Types" to be conventional. But it's not concise. I haven't yet found a reference that provides clear, concise definitions of term, type, kind, and sort. $\endgroup$ – minopret May 6 '13 at 16:02
  • $\begingroup$ What about production heads in a parser? Alot of times you end up classifying grammars under similar names like Expression or Type. $\endgroup$ – CMCDragonkai Feb 2 '16 at 4:13
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ It seems to me as if "sorts" was used with its usual English meaning here, synonymous to "kinds". $\endgroup$ – Raphael Aug 7 '14 at 8:03
  • $\begingroup$ @Raphael Yes, but it seems like that meaning is consistent with the latter formal usage, wouldn't you agree? $\endgroup$ – jcora Aug 7 '14 at 10:24
  • $\begingroup$ Not quite. The phrase "this sort of X" may appear often in the book; this sentence does not signal in any way that something is being defined. (Also, this passage does not match how I understand the term "sort"). $\endgroup$ – Raphael Aug 7 '14 at 12:25
  • $\begingroup$ @Raphael OK, please explain how this particular usage is inconsistent, it would certainly inform me, because that's how I currently understand it. $\endgroup$ – jcora Aug 7 '14 at 13:15
  • $\begingroup$ The notion of "sort" I know is associated with individual nodes of the AST, not a whole tree (which is what you say "phrase" means in your source). $\endgroup$ – Raphael Aug 7 '14 at 14:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.