The Orc typechecker uses a type inference algorithm to deduce type information from a program without any help from the programmer. In many contexts, the typechecker can find all of the type information it needs; however, there are some cases where extra information is needed. For this purpose, there are four kinds of type information that may be added to an Orc program.
Note that due to the erasure property of the Orc type system, adding type information will never change the runtime behavior of the program.
Type information may be added to a polymorphic site or function call
by providing explicit type arguments. The typechecker can usually infer type arguments,
but there are certain cases where it does not have enough information, such as when
calling polymorphic factory sites like Channel
or Ref
.
Whenever a function is defined, in order for the typechecker to determine its type, the definition must be accompanied by information about the argument types and return type of the function. If the function is polymorphic, the names of its type parameters must also be given. This is the same information that a function type carries. There are multiple ways to provide this information, and some of it can be inferred under certain conditions.
The most comprehensive way to provide type information about a function is through a signature. A signature precedes a function definition, providing a sequence of type parameters, a sequence of argument types, and a return type.
|
Type information may also be written directly into a clause of a function definition. For example, the following definitions are equivalent:
{- Adding type information using a signature -} def min(Number, Number) :: Number def min(x,y) = if (x <: y) then x else y {- Inline type information -} def min(x :: Number, y :: Number) :: Number = if (x <: y) then x else y
If the function is not recursive, then the inline return type is optional, because the typechecker can infer the return type from the body expression.
When writing a lambda
expression, type information
must be included in this way, since there is no way to write a separate signature. The return type
is not needed, since a lambda
will never be recursive. The parameter types are required and cannot
be inferred, except in one context: when a lambda
expression appears as an argument to a call which
requires no other inference, then the argument types can be inferred from the type of the target.
|
A pattern may specify the type of values against which it may be matched. The typechecker can then verify this stated type, rather than attempting to infer it, which may provide enough type information to make other inferences possible or resolve ambiguities. Furthermore, adding extra type information makes it easier to pinpoint the source of a typechecking failure. Note that this type information has no effect on the runtime match behavior of the pattern.
|
An expression may specify the type of values that it will publish. The typechecker can then verify this stated type, rather than attempting to infer it, which may provide enough type information to make other inferences possible or resolve ambiguities. 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.
Related Reference Topics
Related Tutorial Sections