Entorno de escritura

En la teoría de tipos , un entorno de tipado (o contexto de tipado ) representa la asociación entre los nombres de las variables y los tipos de datos .

Más formalmente, un entorno${\displaystyle \Gamma }$es un conjunto o lista ordenada de pares${\displaystyle \langle x,\tau \rangle }$, generalmente escrito como${\displaystyle x:\tau }$, dónde${\displaystyle x}$es una variable y${\displaystyle \tau }$su tipo.

El juicio

${\displaystyle \Gamma \vdash e:\tau }$

se lee como "${\displaystyle e}$tiene tipo${\displaystyle \tau }$en contexto${\displaystyle \Gamma }$". ^{[ 1 ]}

Para cada tipo de cuerpo de función, se realizan las siguientes comprobaciones:

${\displaystyle \Gamma =\{(f,\tau _{1}\times ...\times \tau _{n}\to \tau _{0})|(f,xs,(\tau _{1},...,\tau _{n}),t_{f},\tau _{0})\in e\}}$

Ejemplo de reglas de mecanografía: $${\displaystyle {\begin{array}{c}\Gamma \vdash b:Bool,\Gamma \vdash t_{1}:\tau ,\Gamma \vdash t_{2}:\tau \\\hline \Gamma \vdash ({\text{si}}(b)t_{1}{\text{en otro caso}}t_{2}):\tau \\\end{array}}}$$

En los lenguajes de programación de tipado estático , estos entornos se utilizan y mantienen mediante reglas de tipado para verificar el tipo de un programa o expresión dados. ^{[ 1 ]}

• Sistema de tipos