Each of the Orc constants has the expected type:

Orc allows subtyping: some types are included in other types. For example, Integer is a subtype of Number, because all Integers are also Numbers.

Each of the primitive operators typechecks in the obvious way; for example && requires two Boolean operands and returns a Boolean result. Some of the arithmetic operators also support ad-hoc polymorphism; for example, a + expression with two Integer operands has type Integer, but with one or more Number operands it instead has type Number.

There are two other important types: Top and Bot.

Top is the universal type; it is the type of any value, and all other types are subtypes of it.

Bot is the empty type; no value has type Bot. It is a subtype of all other types. Expressions with type Bot are expressions that the typechecker can verify will never publish any values. In particular, stop will never publish, so it has type Bot.

Bot has an interesting status in Orc. In other typed languages, if an expression has type Bot, this usually indicates a guaranteed error, infinite loop, or other failure to return a value. Since sequential programming rarely involves subexpressions that are guaranteed never to return, Bot is usually just a curiosity or a formal artifact of the type system, and indeed many static type systems do not have a Bot type at all. In Orc, however, Bot is very useful, since it is frequently the case that Orc expressions are written to carry out ongoing concurrent activities but never publish any values, and the type system can use the type Bot to indicate that no publications will ever be seen from such expressions.

The type of a tuple is a tuple of the types of each of its elements.

In the conditional expression if E then F else G, the expression E must have type Boolean, and the type of the whole expression is the join of the types of F and G, as described for the parallel combinator.

Though the typechecker can infer the types of many expressions without additional information from the programmer, there are some cases where the algorithm does need assistance. In particular, whenever a function is defined (using the def keyword), the programmer must also include a signature for that function, supplying its argument types and return type.

A signature immediately precedes a function definition, and is written as follows:

def magsq(Number, Number) :: Number
def magsq(x,y) = x*x + y*y

def magsq(Number, Number)
def magsq(x,y) = x*x + y*y

It is also possible to include the argument types and return type directly in a definition, rather than as a separate signature. The signature and definition above could be written together as:

def magsq(x :: Number, y :: Number) :: Number = x*x + y*y

lambda expressions are a special case: the type information must be included directly in this way, since there is no way to declare the signature separately. Specifying the return type of a lambda is always optional, since it is not possible for an anonymous function to make a recursive call. Written as a typed lambda function, the magsq definition looks like:

lambda (x :: Number, y :: Number) = x*x + y*y

Once defined, functions are values, and thus have a special type of their own. The type of a function is written very much like a signature, but using the lambda keyword instead of def and the function name.

In addition to annotation defined functions with a signature, the typechecker can also accept programmer-supplied type information for any expression. An ascription, written E :: T, asks the typechecker to verify that expression E has type T.

Normally, the typechecker would simply find the type of E by inference, but in certain situations it is easier to check a given type. For example, the typechecker may not be able to infer the correct join type for a parallel combinator, but it is always able to check that both branches are subtypes of an already provided type. Furthermore, adding extra type information makes it easier to pinpoint the source of a typechecking failure.

Ascriptions are also allowed in patterns; P :: T is a valid pattern, instructing the typechecker to verify that the value fragment bound by the pattern P will always be of type T.

-- A rectangle is defined by its lower left and upper right coordinates.
type Rect = ((Number, Number), (Number, Number))

-- Transpose such a rectangle, rotating it around an x=y axis
def flip(Rect) :: Rect
def flip( ((a, b), (c, d)) ) = ((a, b), (d, c))

{- 
  Rect(w,h): A rectangle with width w and height h. 
  Circle(r): A circle with radius r.
  RegularPolygon(n,l): A regular polygon with n sides, each of length l.
-}
type Shape = Rect(Number, Number) | Circle(Number) | RegularPolygon(Integer, Number)

When an external site is made available to Orc with the site declaration, its type is also made available to the Orc typechecker. The type of a site is itself treated like a service; it is passed the types of its arguments, and responds with a return type for those arguments. Thus, a site call can typecheck in ways not possible for function calls or other expressions. For example, sites can support ad-hoc polymorphism. Also, sites can respond to messages sent using the dot operator. In fact, Orc has no native record type, because the dot operator only applies to sites, so the type of the site can interpret the message internally and determine the correct type to return, if any.

Additionally, a site can introduce new types into Orc. For example, the Semaphore site responds with new instances of semaphores. And just as sites can be declared using site, these types can be declared using type. Typically they are represented as Java classes, just as sites are. As an example, here is a program which declares the Semaphore type, and then defines a function which "toggles" a pair of semaphores by acquiring the first and releasing the second.

type Semaphore = orc.lib.state.types.SemaphoreType

def toggle(Semaphore, Semaphore) :: Top
def toggle(s, t) = s.acquire() >> t.release()

type definitions occur alongside site definitions in the standard library, so the types returned by many of the library functions are already available.

While the typechecker can be helpful, it will not accept programs that are not safe according to its algorithm, which can be burdensome when the programmer knows that an expression will have a certain type but the typechecker cannot verify it.

Since the typechecker is optional, it can always be turned off in these cases. But this is often too drastic a solution: typechecking difficulties often arise from small segments of a much larger program, and the rest of the program still benefits from typechecking.

Fortunately, the typechecker can be selectively disabled for parts of a program. For this purpose, the typechecker supports a special operation called an assertion, written E :!: T, where E is an expression and T is its asserted type. An assertion is used like an ascription, but rather than verifying that E has type T, the typechecker instead assumes that E has type T, without inspecting E at all. Thus, the programmer can supply the correct type T without being restricted by the typechecking algorithm.

This feature should be used sparingly, with the knowledge that it does compromise the integrity of the typechecking algorithm. If the supplied type is wrong, runtime type errors could propagate to any part of the program that depends on that type. Assertions are useful for rapid prototyping, but they are not recommended for production code.