Editing Typing rule

{{short description|How a type system assigns a type to a syntactic construction}}

In [[type theory]], a '''typing rule''' is an [[inference rule]] that describes how a [[type system]] assigns a type to a [[Syntax (programming languages)|syntactic]] construction.<ref name="TAPL">{{cite book |last1=Pierce |first1=Benjamin C. |title=Types and Programming Languages |date=2002 |publisher=MIT Press |location=Cambridge, Mass. |isbn=0262162091 |edition=1st}}</ref>{{rp|94}} These rules may be applied by the type system to determine if a [[Computer program|program]] is well-typed and what type [[Expression (computer science)|expression]]s 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]].<ref>{{cite web |last1=Baez |first1=John |title=The n-Category Café |url=https://golem.ph.utexas.edu/category/2006/08/cartesian_closed_categories_an_1.html |website=golem.ph.utexas.edu |access-date=30 September 2022 |language=en}}</ref>

== Notation ==
Typing rules specify the structure of a ''typing [[Relation (mathematics)|relation]]'' that relates syntactic terms to their types.<ref name="TAPL" />{{rp|92}} Syntactically, the typing relation is usually denoted by a colon, so for example <math>e:\tau</math> denotes that an expression <math>e</math> has type <math>\tau</math>. The rules themselves are usually specified using the notation of [[natural deduction]].<ref name="TAPL" />{{rp|26}} For example, the following typing rules specify the typing relation for a simple language of [[Boolean data type|booleans]]:<ref name="TAPL" />{{rp|93}}

:<math>
\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}
</math>

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 (computer science)|variable]] depends on where it is [[bound variable|bound]], which necessitates context-sensitive typing rules. These rules are given by a ''typing [[Judgment (mathematical logic)|judgment]]'', usually written <math>\Gamma \vdash e : \tau</math>, which states that an expression <math>e</math> has type <math>\tau</math> under a [[typing context]] <math>\Gamma</math> that relates variables to their types. Typing contexts are occasionally supplemented by the types of individual variables; for example, <math>\Gamma,x{:}\tau_1 \vdash e : \tau_2</math> can be read as "the context <math>\Gamma</math> supplemented by the information that the expression <math>x</math> has type <math>\tau_1</math> yields the judgement that expression <math>e</math> has type <math>\tau_2</math>". This notation can be used to give typing rules for variable references and lambda abstraction in the [[simply typed lambda calculus]]:<ref name="TAPL" />{{rp|pages=101–102}}

:<math>
\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}
</math>

Similarly, the following typing rule describes the <math>\mathbf{let}</math> construct of [[Standard ML]]:

:<math>
\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}
</math>

Not all systems of typing rules directly specify a [[type checking]] algorithm. For example, the typing rule for applying a [[parametric polymorphism|parametrically polymorphic]] function in the [[Hindley–Milner type system]] requires "guessing" the appropriate type at which the function should be instantiated.<ref>{{cite book |last1=Clément |first1=Dominique |last2=Despeyroux |first2=Thierry |last3=Kahn |first3=Gilles |last4=Despeyroux |first4=Joëlle |title=Proceedings of the 1986 ACM conference on LISP and functional programming - LFP '86 |chapter=A simple applicative language: Mini-ML |date=8 August 1986 |pages=13–27 |doi=10.1145/319838.319847 |chapter-url=https://dl.acm.org/doi/10.1145/319838.319847 |publisher=Association for Computing Machinery|isbn=0897912004 |s2cid=5126579 |url=https://hal.inria.fr/inria-00076025/file/RR-0529.pdf }}</ref> Adapting a declarative rule system to a [[Decidability (logic)|decidable]] algorithm requires the production of a separate, algorithmic system that can be proven to specify the same typing relation.<ref>{{cite journal |last1=Dunfield |first1=Jana |last2=Krishnaswami |first2=Neel |title=Bidirectional Typing |journal=ACM Computing Surveys |date=23 May 2021 |volume=54 |issue=5 |page=98:19 |doi=10.1145/3450952 |s2cid=201058734 |issn=0360-0300|doi-access=free |arxiv=1908.05839 }}</ref>

==See also==
* [[Judgment (mathematical logic)]]
* [[Type system]]
* [[Type theory]]
* [[Curry–Howard correspondence]]
* [[Sequent calculus]]

== References ==
{{Reflist}}

== Further reading ==
*  {{cite journal |first=Luca |last=Cardelli |url=https://dl.acm.org/doi/pdf/10.1145/234313.234418 |title=Type Systems |journal=ACM Computing Surveys |date=March 1996 |volume=28 |issue=1 |pages=263–264 |doi=10.1145/234313.234418 |doi-access=free|s2cid=227408784 }}
<!-- I attempted to use this template but got unsure if it was the proper one so I wrote it manually down in the next bullet point after this comment.

* {{cite book |editor-first1=Allen B.  |editor-last1=Tucker |last=Cardelli |first=Luca |date=2004 |title=Computer Science Handbook |url=http://lucacardelli.name/papers/typesystems.pdf |chapter=97 |location= |publisher=Chapman and Hall/CRC |isbn=9780429209390 |access-date=5 January 2025}} -->
* Cardelli, Luca (June 2004). [http://lucacardelli.name/papers/typesystems.pdf Type Systems], 41 pages. Computer Science Handbook, 2nd Edition, Ch. 97. Edited by Allen B. Tucker. ISBN 9780429209390. Retrieved 5 January 2025.

{{type-theory-stub}}

[[Category:Data types]]
[[Category:Program analysis]]
[[Category:Type theory]]