9.1. Metatheory

The typechecker uses the local type inference algorithm described by Pierce and Turner in the paper Local Type Inference. The typechecker extends this algorithm with polymorphic type operators (e.g. List or Channel), forming a second-order type system. It also includes polymorphic user-defined datatypes and a typing procedure for site calls.

The typechecker supports both generics and subtyping, though it does not currently implement bounded polymorphism, which combines the two. Sites may also be overloaded (ad-hoc polymorphism), but the programmer cannot write overloaded functions within Orc itself.

The Orc type system currently uses an erasure semantics, meaning that type information does not affect runtime behavior, and may be removed from a program after typechecking is finished. In the case of datatype declarations, the type information and constructor bindings are separated by the compiler, so that datatypes may be used in an untyped setting.

9.1.1. Related Links

Related Tutorial Sections