Sistema F

El sistema F (también conocido como cálculo lambda polimórfico o cálculo lambda de segundo orden ) es un cálculo lambda tipado que introduce, al cálculo lambda tipado simple , un mecanismo de cuantificación universal sobre tipos. El sistema F formaliza el polimorfismo paramétrico en lenguajes de programación , constituyendo así la base teórica de lenguajes como Haskell y ML . Fue descubierto independientemente por el lógico Jean-Yves Girard (1972) y el informático John C. Reynolds .

Mientras que el cálculo lambda tipado simple tiene variables que abarcan términos y ligaduras para ellos, el Sistema F además tiene variables que abarcan tipos y ligaduras para ellos. Como ejemplo, el hecho de que la función identidad pueda tener cualquier tipo de la forma A → A se formalizaría en el Sistema F como la declaración

${\displaystyle \vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha }$

dónde${\displaystyle \alpha }$es una variable de tipo . La mayúscula${\displaystyle \Lambda }$se utiliza tradicionalmente para denotar funciones de nivel de tipo, a diferencia de la minúscula${\displaystyle \lambda }$que se utiliza para funciones de nivel de valor. (El superíndice${\displaystyle \alpha }$significa que la variable ligada x es de tipo${\displaystyle \alpha }$La expresión que aparece después de los dos puntos es del tipo de la expresión lambda que la precede.

Como sistema de reescritura de términos , el Sistema F es fuertemente normalizador . Sin embargo, la inferencia de tipos en el Sistema F (sin anotaciones de tipo explícitas) es indecidible . Bajo el isomorfismo de Curry-Howard , el Sistema F corresponde a la lógica intuicionista proposicional de segundo orden . El Sistema F puede considerarse parte del cubo lambda , junto con cálculos lambda tipados aún más expresivos, incluidos aquellos con tipos dependientes .

Según Girard, la "F" en Sistema F fue elegida al azar. ^{[ 1 ]}

Las reglas de tipado del Sistema F son las del cálculo lambda simplemente tipado con la adición de lo siguiente:

dónde${\displaystyle \sigma ,\tau }$son tipos,${\displaystyle \alpha }$es una variable de tipo y${\displaystyle \alpha ~{\text{tipo}}}$en el contexto indica que${\displaystyle \alpha }$está ligado. La primera regla es la de aplicación, y la segunda es la de abstracción. ^{[ 2 ] [ 3 ]}

El${\displaystyle {\mathsf {Booleano}}}$El tipo se define como: ${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$, dónde${\displaystyle \alpha }$es una variable de tipo . Esto significa:${\displaystyle {\mathsf {Booleano}}}$es el tipo de todas las funciones que toman como entrada un tipo α y dos expresiones de tipo α , y producen como salida una expresión de tipo α (nótese que consideramos${\displaystyle \to }$ser asociativo por la derecha .)

Las dos definiciones siguientes para los valores booleanos${\displaystyle \mathbf {T} }$y${\displaystyle \mathbf {F} }$se utilizan, extendiendo la definición de booleanos de Church :

${\displaystyle \mathbf {T} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}x}$

${\displaystyle \mathbf {F} =\Lambda \alpha {.}\lambda x^{\alpha }\lambda y^{\alpha }{.}y}$

(Tenga en cuenta que las dos funciones anteriores requieren tres argumentos , no dos . Los dos últimos deben ser expresiones lambda, pero el primero debe ser un tipo. Este hecho se refleja en el hecho de que el tipo de estas expresiones es${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$; el cuantificador universal que une α corresponde a Λ que une alfa en la expresión lambda misma. Además, tenga en cuenta que${\displaystyle {\mathsf {Booleano}}}$es una abreviatura conveniente para${\displaystyle \forall \alpha .\alpha \to \alpha \to \alpha }$, pero no es un símbolo del Sistema F en sí mismo, sino más bien un "metasimbo". Del mismo modo,${\displaystyle \mathbf {T} }$y${\displaystyle \mathbf {F} }$También son "metasimbos", abreviaturas convenientes, de "ensamblajes" del Sistema F (en el sentido de Bourbaki ); de lo contrario, si tales funciones pudieran nombrarse (dentro del Sistema F), entonces no habría necesidad del aparato de expresiones lambda capaz de definir funciones de forma anónima ni del combinador de punto fijo , que sortea esa restricción.

Luego, con estos dos${\displaystyle \lambda }$-términos, podemos definir algunos operadores lógicos (que son de tipo${\displaystyle {\mathsf {Booleano}}\rightarrow {\mathsf {Booleano}}\rightarrow {\mathsf {Booleano}}}$):

${\displaystyle {\begin{aligned}\mathrm {AND} &=\lambda x^{\mathsf {Booleano}}\lambda y^{\mathsf {Booleano}}{.}x\,{\mathsf {Booleano}}\,y\,\mathbf {F} \\\mathrm {OR} &=\lambda x^{\mathsf {Booleano}}\lambda y^{\mathsf {Booleano}}{.}x\,{\mathsf {Booleano}}\,\mathbf {T} \,y\\\mathrm {NOT} &=\lambda x^{\mathsf {Booleano}}{.}x\,{\mathsf {Booleano}}\,\mathbf {F} \,\mathbf {T} \end{alineado}}}$

Tenga en cuenta que en las definiciones anteriores,${\displaystyle {\mathsf {Booleano}}}$es un argumento de tipo para${\displaystyle x}$, especificando que los otros dos parámetros que se dan a${\displaystyle x}$son de tipo${\displaystyle {\mathsf {Booleano}}}$. Al igual que en las codificaciones de Church, no es necesario usar una función IFTHENELSE , ya que se puede usar directamente${\displaystyle {\mathsf {Booleano}}}$-términos tipificados como funciones de decisión. Sin embargo, si se solicita uno:

${\displaystyle \mathrm {IFTENELSE} =\Lambda \alpha .\lambda x^{\mathsf {Booleano}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

lo haré. Un predicado es una función que devuelve un${\displaystyle {\mathsf {Booleano}}}$valor de tipo. El predicado más fundamental es ISZERO que devuelve${\displaystyle \mathbf {T} }$si y solo si su argumento es el numeral eclesiástico 0 :

${\displaystyle \mathrm {ISZERO} =\lambda n^{\forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }{.}n\,{\mathsf {Boolean}}\,(\lambda x^{\mathsf {Boolean}}{.}\mathbf {F} )\,\mathbf {T} }$

Además, el cuantificador existencial (y por lo tanto los tipos existenciales) se pueden implementar en el sistema F de la siguiente manera: ^{[ 4 ] [ 5 ]}

${\displaystyle \exists X.A=\forall Y.(\forall X.A\rightarrow Y)\rightarrow Y}$

El sistema F permite que las construcciones recursivas se incrusten de forma natural, de manera similar a la teoría de tipos de Martin-Löf . Las estructuras abstractas ( S ) se crean mediante constructores . Estas son funciones tipificadas como:

${\displaystyle K_{1}\rightarrow K_{2}\rightarrow \dots \rightarrow S}$.

La recursividad se manifiesta cuando S mismo aparece dentro de uno de los tipos.${\displaystyle K_{i}}$. Si tienes m de estos constructores, puedes definir el tipo de S como:

${\displaystyle \forall \alpha .(K_{1}^{1}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\dots \rightarrow (K_{1}^{m}[\alpha /S]\rightarrow \dots \rightarrow \alpha )\rightarrow \alpha }$

Por ejemplo, los números naturales se pueden definir como un tipo de dato inductivo N con constructores

${\displaystyle {\begin{aligned}{\mathit {zero}}&:\mathrm {N} \\{\mathit {succ}}&:\mathrm {N} \rightarrow \mathrm {N} \end{aligned}}}$

El tipo de sistema F correspondiente a esta estructura es ${\displaystyle \forall \alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$Los términos de este tipo comprenden una versión mecanografiada de los numerales eclesiásticos , los primeros de los cuales son:

${\displaystyle {\begin{aligned}0&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.x\\1&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.fx\\2&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(fx)\\3&:=\Lambda \alpha .\lambda x^{\alpha }.\lambda f^{\alpha \to \alpha }.f(f(fx))\end{aligned}}}$

Si invertimos el orden de los argumentos currificados ( es decir,${\displaystyle \forall \alpha .(\alpha \rightarrow \alpha )\rightarrow \alpha \rightarrow \alpha }$), entonces el numeral de Church para n es una función que toma una función f como argumento y devuelve la n ^-ésima potencia de f . Es decir, un numeral de Church es una función de orden superior : toma una función f de un solo argumento y devuelve otra función de un solo argumento.

La versión del Sistema F utilizada en este artículo es un cálculo con tipado explícito, o de estilo Church. La información de tipado contenida en los términos λ simplifica la verificación de tipos . Joe Wells (1994) resolvió un "problema abierto embarazoso" al demostrar que la verificación de tipos es indecidible para una variante de estilo Curry del Sistema F, es decir, una que carece de anotaciones de tipado explícitas. ^{[ 6 ] [ 7 ]}

El resultado de Wells implica que la inferencia de tipos para el Sistema F es imposible. Una restricción del Sistema F conocida como " Hindley-Milner ", o simplemente "HM", sí tiene un algoritmo de inferencia de tipos sencillo y se utiliza para muchos lenguajes de programación funcional con tipado estático, como Haskell 98 y la familia ML . Con el tiempo, a medida que las restricciones de los sistemas de tipos de estilo HM se han hecho evidentes, los lenguajes han evolucionado progresivamente hacia lógicas más expresivas para sus sistemas de tipos. GHC , un compilador de Haskell, va más allá de HM (desde 2008) y utiliza el Sistema F extendido con igualdad de tipos no sintáctica; ^{[ 8 ]} las características no HM en el sistema de tipos de OCaml incluyen GADT . ^{[ 9 ] [ 10 ]}

En la lógica intuicionista de segundo orden , el cálculo lambda polimórfico de segundo orden (F2) fue descubierto por Girard (1972) e independientemente por Reynolds (1974). ^{[ 11 ]} Girard demostró el teorema de representación : que en la lógica de predicados intuicionista de segundo orden (P2), las funciones de los números naturales a los números naturales que pueden demostrarse totales forman una proyección de P2 en F2. ^{[ 11 ]} Reynolds demostró el teorema de abstracción : que cada término en F2 satisface una relación lógica, que puede incrustarse en las relaciones lógicas P2. ^{[ 11 ]} Reynolds demostró que una proyección de Girard seguida de una incrustación de Reynolds forman la identidad, es decir, el isomorfismo de Girard-Reynolds . ^{[ 11 ]}

Mientras que el Sistema F corresponde al primer eje del cubo lambda de Barendregt , el Sistema F _ω o el cálculo lambda polimórfico de orden superior combina el primer eje (polimorfismo) con el segundo eje ( operadores de tipo ); es un sistema diferente y más complejo.

El sistema F _ω puede definirse inductivamente en una familia de sistemas, donde la inducción se basa en los tipos permitidos en cada sistema:

• ${\displaystyle F_{n}}$tipos de permisos:
  • ${\displaystyle \star }$(el tipo de tipos) y
  • ${\displaystyle J\Rightarrow K}$dónde${\displaystyle J\in F_{n-1}}$y${\displaystyle K\in F_{n}}$(el tipo de funciones que transforman tipos en tipos, donde el tipo de argumento es de orden inferior)

En el límite, podemos definir el sistema${\displaystyle F_{\omega }}$ser

• ${\displaystyle F_{\omega }={\underset {1\leq i}{\bigcup }}F_{i}}$

Es decir, F _ω es el sistema que permite funciones de tipos a tipos donde el argumento (y el resultado) pueden ser de cualquier orden.

Tenga en cuenta que, si bien F _ω no impone restricciones en el orden de los argumentos en estas asignaciones, sí restringe el universo de los argumentos para estas asignaciones: deben ser tipos en lugar de valores. El sistema F _ω no permite asignaciones de valores a tipos ( tipos dependientes ), aunque sí permite asignaciones de valores a valores (${\displaystyle \lambda }$abstracción), asignaciones de tipos a valores (${\displaystyle \Lambda }$abstracción) y asignaciones de tipos a tipos (${\displaystyle \lambda }$abstracción a nivel de tipos).

El sistema F _{< :} , pronunciado "F-sub", es una extensión del sistema F con subtipado . El sistema F _{< :} ha sido de vital importancia para la teoría de los lenguajes de programación desde la década de 1980 porque el núcleo de los lenguajes de programación funcional , como los de la familia ML , admite tanto el polimorfismo paramétrico como el subtipado de registros , que se puede expresar en el sistema F _{< :} . ^{[ 12 ] [ 13 ]}

• Tipos existenciales : las contrapartes cuantificadas existencialmente de los tipos universales.
• Sistema U
• cubo Lambda

• Pierce, Benjamin (2002). "V Polymorphism Cap. 23. Universal Types, Cap. 25. An ML Implementation of System F" . Types and Programming Languages . MIT Press. pp. 339–362 , 381–388 . ISBN  0-262-16209-1.

• Resumen del Sistema F de Franck Binard.
• Sistema F _ω : el caballo de batalla de los compiladores modernos por Greg Morrisett