Typing rules specify the structure of a typing relation that relates syntactic terms to their types.[1]: 92 Syntactically, the typing relation is usually denoted by a colon, so for example denotes that an expression has type . The rules themselves are usually specified using the notation of natural deduction.[1]: 26 For example, the following typing rules specify the typing relation for a simple language of booleans:[1]: 93
Each rule states that the conclusion below the line may be derived from the premises above the line. The first two rules have no premises above the line, so they are axioms. The third rule has premises above the line (specifically, three premises), so it is an inference rule.
In programming languages, the type of a variable depends on where it is bound, which necessitates context-sensitive typing rules. These rules are given by a typing judgment, usually written , which states that an expression has type under a typing context that relates variables to their types. Typing contexts are occasionally supplemented by the types of individual variables; for example, can be read as "the context supplemented by the information that the expression has type yields the judgement that expression has type ". This notation can be used to give typing rules for variable references and lambda abstraction in the simply typed lambda calculus:[1]: 101–102
Similarly, the following typing rule describes the construct of Standard ML:
Not all systems of typing rules directly specify a type checking algorithm. For example, the typing rule for applying a parametrically polymorphic function in the Hindley–Milner type system requires "guessing" the appropriate type at which the function should be instantiated.[3] Adapting a declarative rule system to a decidable algorithm requires the production of a separate, algorithmic system that can be proven to specify the same typing relation.[4]
^ abcdePierce, Benjamin C. (2002). Types and Programming Languages (1st ed.). Cambridge, Mass.: MIT Press. ISBN0262162091.
^Baez, John. "The n-Category Café". golem.ph.utexas.edu. Retrieved 30 September 2022.
^Clément, Dominique; Despeyroux, Thierry; Kahn, Gilles; Despeyroux, Joëlle (8 August 1986). "A simple applicative language: Mini-ML". Proceedings of the 1986 ACM conference on LISP and functional programming - LFP '86(PDF). Association for Computing Machinery. pp. 13–27. doi:10.1145/319838.319847. ISBN0897912004. S2CID 5126579.
typing, rule, type, theory, typing, rule, inference, rule, that, describes, type, system, assigns, type, syntactic, construction, these, rules, applied, type, system, determine, program, well, typed, what, type, expressions, have, prototypical, example, typing. In type theory a typing rule is an inference rule that describes how a type system assigns a type to a syntactic construction 1 94 These rules may be applied by the type system to determine if a program is well typed and what type expressions have A prototypical example of the use of typing rules is in defining type inference in the simply typed lambda calculus which is the internal language of Cartesian closed categories 2 Contents 1 Notation 2 See also 3 References 4 Further readingNotation editTyping rules specify the structure of a typing relation that relates syntactic terms to their types 1 92 Syntactically the typing relation is usually denoted by a colon so for example e t displaystyle e tau nbsp denotes that an expression e displaystyle e nbsp has type t displaystyle tau nbsp The rules themselves are usually specified using the notation of natural deduction 1 26 For example the following typing rules specify the typing relation for a simple language of booleans 1 93 t r u e B o o l f a l s e B o o l e 1 B o o l e 2 t e 3 t i f e 1 t h e n e 2 e l s e e 3 t displaystyle frac mathsf true mathsf Bool qquad frac mathsf false mathsf Bool qquad frac e 1 mathsf Bool quad e 2 tau quad e 3 tau mathbf if e 1 mathbf then e 2 mathbf else e 3 tau nbsp Each rule states that the conclusion below the line may be derived from the premises above the line The first two rules have no premises above the line so they are axioms The third rule has premises above the line specifically three premises so it is an inference rule In programming languages the type of a variable depends on where it is bound which necessitates context sensitive typing rules These rules are given by a typing judgment usually written G e t displaystyle Gamma vdash e tau nbsp which states that an expression e displaystyle e nbsp has type t displaystyle tau nbsp under a typing context G displaystyle Gamma nbsp that relates variables to their types Typing contexts are occasionally supplemented by the types of individual variables for example G x t 1 e t 2 displaystyle Gamma x tau 1 vdash e tau 2 nbsp can be read as the context G displaystyle Gamma nbsp supplemented by the information that the expression x displaystyle x nbsp has type t 1 displaystyle tau 1 nbsp yields the judgement that expression e displaystyle e nbsp has type t 2 displaystyle tau 2 nbsp This notation can be used to give typing rules for variable references and lambda abstraction in the simply typed lambda calculus 1 101 102 x t G G x t G x t 1 e t 2 G l x t 1 e t 1 t 2 displaystyle frac x tau in Gamma Gamma vdash x tau qquad frac Gamma x tau 1 vdash e tau 2 Gamma vdash lambda x tau 1 e tau 1 rightarrow tau 2 nbsp Similarly the following typing rule describes the l e t displaystyle mathbf let nbsp construct of Standard ML G e 1 t 1 G x t 1 e 2 t 2 G l e t x e 1 i n e 2 e n d t 2 displaystyle frac Gamma vdash e 1 tau 1 qquad Gamma x tau 1 vdash e 2 tau 2 Gamma vdash mathbf let x e 1 mathbf in e 2 mathbf end tau 2 nbsp Not all systems of typing rules directly specify a type checking algorithm For example the typing rule for applying a parametrically polymorphic function in the Hindley Milner type system requires guessing the appropriate type at which the function should be instantiated 3 Adapting a declarative rule system to a decidable algorithm requires the production of a separate algorithmic system that can be proven to specify the same typing relation 4 See also editJudgment mathematical logic Type system Type theory Curry Howard correspondence Sequent calculusReferences edit a b c d e Pierce Benjamin C 2002 Types and Programming Languages 1st ed Cambridge Mass MIT Press ISBN 0262162091 Baez John The n Category Cafe golem ph utexas edu Retrieved 30 September 2022 Clement Dominique Despeyroux Thierry Kahn Gilles Despeyroux Joelle 8 August 1986 A simple applicative language Mini ML Proceedings of the 1986 ACM conference on LISP and functional programming LFP 86 PDF Association for Computing Machinery pp 13 27 doi 10 1145 319838 319847 ISBN 0897912004 S2CID 5126579 Dunfield Jana Krishnaswami Neel 23 May 2021 Bidirectional Typing ACM Computing Surveys 54 5 98 19 doi 10 1145 3450952 ISSN 0360 0300 S2CID 201058734 Further reading editCardelli Luca March 1996 Type Systems PDF ACM Computing Surveys 28 1 263 264 doi 10 1145 234313 234418 S2CID 227408784 G displaystyle Gamma vdash nbsp This programming language theory or type theory related article is a stub You can help Wikipedia by expanding it vte Retrieved from https en wikipedia org w index php title Typing rule amp oldid 1173439835, wikipedia, wiki, book, books, library,