Top-down typing strategy - is there a name for this?

In most statically typed languages, each expression has an intrinsic type. E.g. in Java, 3 is an int, 3.0 is a double, 3+3.0 is also a double. Types do not depend on the context of the expression.

However, in the CSS type system described in the spec, some expressions have a type depending on the context. For example, the red token can be a <color>, a <custom-ident>, or an <attr-name>, depending on the context in which it is used.

I want to build a type system for a CSS-based programming langauge. In this type system, I want to use a typing strategy that does not go from the bottom up (starting from the leaves in the AST), but top down (starting from the root of the AST).

For example, when the compiler needs to derive that the linear(red, yellow) expression inhabits the <bg-image> type, it would do the following derivation:

we want to derive that
linear(red, yellow) :: <bg-image>
<bg-image> is defined as <url> | linear(<color>, <color>), so
linear(red, yellow) :: <url> | linear(<color>, <color>)
let us try the second branch
linear(red, yellow) :: linear(<color>, <color>)
let us check sub-expressions
red :: <color>
yellow :: <color>
everything fine, OK


Can you point me to scholarly articles where this kind of typing strategy is discussed?

P.s. I don't know of other languages where a type of the expression depends on the context, except for Perl. In Perl, ("a","b") can be interpreted as either a list or an integer (its length), depending on the context:

print ("a","b") # => ab
print 0+("a","b") # => 2

• There are many languages were the type of an expression depends on the context. To begin with, nearly all languages assume that the type of the conditional expression in an if-statement is boolean. Top-down or bottom-up is a computation/checking strategy. What you really have is a proof tree to be checked for correctness, where the operator-operand type constraints are the inference rules. – babou Jun 10 '15 at 12:32
• In fact, your first paragraph gives an example where the same expression is cast to a different type for the surrounding expression. (cc @babou) Anyway, is type inference what you want? – Raphael Jun 10 '15 at 12:32
• I think you suffer from a case of operationalitis, a fairly common disease, but harmless if you deal with it with a cure of declarativeness, an excellent drug. You are trying to describe your type system by describing how type correctness should be checked. You should only state the kind of constraints the type system imposes on your programs (such as: the type of a+b is int iff both a and b are of type int). Then, it is for the implementors to worry about checking that operationally. Of course, you try to stay within tractable limits so that they have a chance of doing it. – babou Jun 10 '15 at 12:48
• @Raphael, yes, i didn't realize but it's type inference what I want. Yes in 3+3.0, it is an implicit type conversion. But I want type inference, not implicit type conversion. – Bernát Jun 11 '15 at 16:46
• @babou, :) yes, probably I caught an operationalitis because I tried to be the language designer and the implementor at the same time. – Bernát Jun 11 '15 at 16:47

There is no top-down or bottom-up typing strategy when defining a language. It is an implementation issue. A type system will only define operator operand constraints on your AST. The kind constraints is fixed by the type system and is part of the design of the language. It can be very simple as in older languages, or be a sophisticated logical system. Even when simple, it can be seen as a logical system. Your AST may be seen as a proof tree in that logical system, where the nodes are to be decorated by types, that may be seen as logical propositions proved by by the sub-tree dominated by that node . For example, the type int found for an expression is a predicate satisfied by the expression.

So you can associate type inference rules to the operators of your AST. For example if you have an AST operator + with two operands, you can associate (among others) the inference rule: $X::int \,\wedge\, Y::int \;\Rightarrow\; X+Y::int$

Defining the type system of a language amount to defining such rules for all AST operators where that make sense, i.e. involved with the type system.

Type checking your program consists in finding a type for each (relevant) AST node, such that that there is an inference rule (associated to the operator of that node) that is satisfied by the node type and the types of its operands.

This can be done with top-down or bottom-up algorithms, or any mix. That is only a matter of finding efficient algorithms. But the checking strategy is an implementation issue, not a language definition issue. However, it is advisable to choose a type system that allows for a tractable type checking strategy.

Note that the types may not be all completely defined by the type system, and the checking strategy may actually infer the "details" of these types, in particular by means of unification techniques.

The above description may not seem too complex (I hope). One hidden aspect, that makes the whole thing a lot more interesting, is that in static typing (particularly) all occurences of the same variable must have the same type, which introduces additional constraints. But getting into the details is too much for a normally sized answer.

For more about this, you should look for type inference.

• Wow, I didn't know I was doing type inference :) So, instead of saying the type system is top-down, is it correct to say this: In this type system, the type of a subexpression in an AST cannot be inferred uneqivocally unless we know the type of its parent expression. An example, we want to infer the type of 3 in 3+3. However, the language contains union types, so 3 can be of int, int|string, int|string|boolean etc. The type of 3+3 can also be int, int|string etc. But if we know, from an external type annotation, the type of the root, we can maybe infer types unambiguously. – Bernát Jun 11 '15 at 16:33
• A bit late for me. Basically in general, there is not one place that is responsible for the initial typing. The inference rules create a collection of equation (constraints) to be simultaneously solved. So it is more a question of overall consistency. You can also say that 3 imposes somes types, and the context has to be consistent with them, though it can further restrict the choice. To take it differently, if you had a typing error, you cannot incriminate the context more than whatever happens in the subtree. – babou Jun 12 '15 at 0:06
• @Bernát I don't think you can separate type inference and implicit conversion in such cases. You have assigned/inferred type int for an expression, and then find int + double. If your inferrer is supposed to infer type double for the whole expression, it has to know that there is a conversion from int to double (and it may want to issue a compiler warning regarding potential loss of precision). (Or, alternatively, you'd have to have + for this combination.) – Raphael Jun 12 '15 at 9:21
• @Bernát You may be interested in Scala and its type system; the programmer can define new implicit conversions in Scala which the compiler automatically applies as appropriate, much like the ones between primitive types in Java. – Raphael Jun 12 '15 at 9:21