Definition
Intrinsic typing, also known as Church-style typing, defines terms such that they are inherently typed. The syntax rules enforce that every well-formed term is constructed alongside its type. A term cannot be formulated independently of its type .
Extrinsic typing, also known as Curry-style typing, defines terms as untyped syntactic objects first. Types are subsequently assigned to these pre-existing terms via typing judgments. In this formulation, an untyped term may be assigned no type, one type, or multiple types.
Remarks
- In intrinsic systems, type checking is a prerequisite for term well-Formed Term.
- In extrinsic systems, operational semantics can be evaluated on raw terms independent of their typing derivations.
- Type theories such as Martin-Löf type theory, and proof assistants such as Agda, generally employ intrinsic typing.
- Extrinsic typing naturally accommodates intersection types and polymorphism without explicit type annotations on b,inders.
- Simply-Typed Lambda Calculus is an example of an extrinsicly typed system.