Relación entre la teoría de los tipos de Russell y los sistemas de tipos
12
Recientemente me di cuenta de que hay algún tipo de relación entre la teoría de los tipos de Russell y los sistemas de tipos, como se encuentra, por ejemplo, en Haskell. En realidad, parte de la notación de tipos en Haskell parece tener precursores en la teoría de tipos. Pero, en mi humilde opinión, la motivación de Russell en 1908 fue evitar la paradoja de Russell, y no estoy seguro de cómo se relaciona eso con los sistemas de tipos en informática.
¿Es la paradoja de Russell de una forma u otra algo de lo que deberíamos preocuparnos, por ejemplo, si no tuviéramos un buen sistema de tipos en un idioma determinado?
La "teoría de tipos" en el sentido de los lenguajes de programación y en el sentido de Russell está estrechamente relacionada. De hecho, el campo moderno de la teoría de tipos dependientes tiene como objetivo proporcionar una base constructiva para las matemáticas. A diferencia de la teoría de conjuntos, la mayoría de las investigaciones basadas en la teoría de tipos las matemáticas se realizan en asistentes de pruebas como Coq, NuPRL o Agda. Como tal, las pruebas realizadas en estos sistemas no solo son "formalizables" sino que también son totalmente formales y verificadas por máquina. Mediante tácticas y otras técnicas de automatización de pruebas, intentamos probar con estas sistemas "de alto nivel" y, por lo tanto, se parecen a las matemáticas informales, pero debido a que todo está verificado, tenemos muchas mejores garantías de corrección.
Los tipos en lenguajes de programación ordinarios tienden a ser más limitados, pero la meta teoría es la misma.
Algo similar a la paradoja de Russell es un problema importante en la teoría del tipo dependiente. En particular, teniendo
Type : Type
Por lo general conduce a la contradicción. Coq y trabajo similar al anidar universos
Type_0 : Type_1
pero en Coq por defecto estos números son implícitos ya que normalmente no son importantes para el programador.
En algunos sistemas (Agda, Idris), la regla de tipo en tipo se habilita mediante un indicador de compilación. Hace que la lógica sea inconsistente, pero a menudo facilita la programación / prueba exploratoria.
Incluso en los idiomas más convencionales, la paradoja de Russell ocasionalmente aparece. Por ejemplo, en Haskell, es posible una codificación de la paradoja de Russell que combina la impredicatividad y el caso de tipo abierto, lo que permite construir términos divergentes sin recursividad incluso a nivel de tipo. Haskell es `` inconsistente '' (cuando se interpreta como una lógica de la manera habitual) ya que admite tanto la recursión de nivel de tipo como de valor, sin mencionar excepciones. Sin embargo, este resultado es bastante interesante.
Gracias por su respuesta detallada: en lo que respecta a la prueba, todavía no hay herramientas a la vista para demostrar la corrección de los programas en lenguajes imperativos como C ++ o Java, ¿verdad? Me encantaría poner mis manos en uno de estos ... Me doy cuenta de que esta es una tangente completa. Sé acerca de Coq y Agda, pero no parecían ser las herramientas adecuadas para demostrar la corrección de los programas escritos en C ++ o Java.
Frank
3
Hay algunas herramientas. Algunos para C, muchos para Java y toneladas para Ada. Ver por ejemplo: Why (Java, C, Ada), Krakatoa (Java) o SPARK (subconjunto Ada con herramientas muy buenas). Sin embargo, para C ++, no tanto. También te puede interesar YNot (Coq DSL).
Philip JF
3
Tienes razón sobre la motivación de Russell. Su paradoja plaga todas las teorías de conjuntos que admiten axiomas de comprensión irrestrictos en el sentido de que: cualquier función proposicional determina un conjunto, es decir, la de todas aquellas entidades que satisfacen la función. Entre las teorías basadas en conjuntos que tenían ese defecto estaban la ingenua teoría de conjuntos de Cantor y el sistema de Grundgesetze de Frege (específicamente: axioma 5).
Dado que los tipos se consideran tipos especiales de conjuntos, si no se tiene cuidado, una paradoja similar puede colarse en un sistema de tipos. Dicho esto, no conozco ningún sistema de tipos que haya sufrido tal destino. Solo puedo recordar los primeros intentos de Church de formular el cálculo lambda en los años 30, que resultó ser inconsistente (paradoja de Kleene-Rosser), pero que no se debió a tipos ni a la paradoja de Russell.
Actualización : Vea la respuesta de Philip para una respuesta real a su pregunta.
Gracias por tu respuesta. Probablemente hay alternativas a los tipos a la Russell para evitar la paradoja de Russell. ¿Alguna de estas soluciones alternativas tendría algo interesante que contribuir a los lenguajes informáticos? Los tipos mundanos son muy útiles para especificar claramente los contratos entre partes del código, e incluso antes de eso, para dar semántica a los programas. ¿Habría otras semánticas que podrían obtenerse con algo más que tipos? (No tengo idea de lo que sería :-)
Frank
1
Sí, hay muchas alternativas (Quine's NF, ZFC, etc.), pero no puedo ver ninguna conexión directa entre la crisis fundamental y los lenguajes de programación. Si considera la teoría de tipos de Martin Lof como un lenguaje de programación, puede haber alguna conexión allí que se remonta al intuicionismo. En cuanto a la semántica de los lenguajes de programación, hay algunos lenguajes básicos como PDL (Propositional Dynamic Logic) que tienen semántica de Kripke (o mundos posibles). Pero los tipos me parecen tan fundamentales que podrían estar detrás de escena :)
Hunan Rostomyan
1
Pero los tipos son un fastidio: los quiere y los necesita, pero le encantaría no tener que especificarlos (por lo tanto, en mi humilde opinión, por qué tenemos sistemas de inferencia de tipos en idiomas como Haskell u Ocaml (me encantan esos idiomas)). En el otro extremo del espectro, Python se siente muy intuitivo y es agradable (y eficiente en términos de tiempo de codificación) no tener que preocuparse demasiado por los tipos en ese idioma. Tal vez la inferencia de tipos es lo mejor del mundo, pero ese es el ingeniero hablando. Estaba soñando despierto que las matemáticas podrían contribuir con otro concepto importante (como los tipos) a la informática :-)
Frank
1
@Frank Cada vez que uso un lenguaje sin tipos estáticos (principalmente Ruby) odio la experiencia, porque odio los errores de tiempo de ejecución evitables. Entonces, eso parece ser una cuestión de gustos en su mayoría. Estoy de acuerdo en que la inferencia de tipos poderosa puede darle lo mejor de ambos mundos. Por eso, probablemente, me gusta tanto Scala.
Raphael
No estoy convencido de que no tener tipos "automáticamente" conduzca a errores de tiempo de ejecución, como parece implicar :-) Nunca tuve un problema en Python.
Frank
3
Como mencionas Python, la pregunta no es puramente teórica. Así que trato de dar una perspectiva más amplia sobre los tipos. Los tipos son cosas diferentes para diferentes personas. He recopilado al menos 5 nociones distintas (pero relacionadas) de tipos:
Los sistemas de tipos son sistemas lógicos y teorías de conjuntos.
Un sistema de tipos asocia un tipo con cada valor calculado. Al examinar el flujo de estos valores, un sistema de tipos intenta probar o garantizar que no se produzcan errores de tipo.
Tipo es una clasificación que identifica uno de varios tipos de datos, como valor real, entero o booleano, que determina los valores posibles para ese tipo; las operaciones que se pueden realizar en valores de ese tipo; el significado de los datos; y la forma en que se pueden almacenar valores de ese tipo
Los tipos de datos abstractos permiten la abstracción de datos en lenguajes de alto nivel. Los ADT a menudo se implementan como módulos: la interfaz del módulo declara los procedimientos que corresponden a las operaciones de ADT. Esta estrategia de ocultación de información permite cambiar la implementación del módulo sin perturbar los programas del cliente.
Las implementaciones de lenguaje de programación usan tipos de valores para elegir el almacenamiento que necesitan los valores y algoritmos para las operaciones en los valores.
Las citas son de Wikipedia, pero puedo proporcionar mejores referencias en caso de necesidad.
Los tipos 1 surgieron del trabajo de Russel, pero hoy no solo están protegidos de las paradojas: el lenguaje mecanografiado de la teoría de los tipos de homotopía es una nueva forma de codificar las matemáticas en un lenguaje formal, entendible por la máquina, y una nueva forma para que los humanos entiendan los fundamentos de las matematicas. (La forma "antigua" es codificar usando una teoría de conjuntos axiomática).
Los tipos 2-5 surgieron en la programación a partir de varias necesidades diferentes: evitar errores, clasificar los diseñadores de software de datos y los programadores con los que trabajan, diseñar sistemas grandes e implementar lenguajes de programación de manera eficiente, respectivamente.
Los sistemas de tipos en C / C ++, Ada, Java, Python no surgieron del trabajo de Russel o del deseo de evitar errores. Surgieron de la necesidad de describir diferentes tipos de datos (por ejemplo, "el apellido es una cadena de caracteres y no un número"), modularizar el diseño del software y elegir representaciones de bajo nivel para los datos de manera óptima. Estos idiomas no tienen tipos-1 o tipos-2. Java garantiza una seguridad relativa contra errores no mediante la prueba de la corrección del programa utilizando el sistema de tipos, sino mediante un diseño cuidadoso del lenguaje (sin aritmética de puntero) y el sistema de tiempo de ejecución (máquina virtual, verificación de código de bytes). El sistema de tipos en Java no es un sistema lógico ni una teoría de conjuntos.
Sin embargo, el sistema de tipos en el lenguaje de programación Agda es una variante moderna del sistema de tipos de Russel (basado en trabajos posteriores o de Per Martin-Lof y otros matemáticos). El sistema de tipos en Agda está diseñado para expresar las propiedades matemáticas del programa y las pruebas de esas propiedades, es un sistema lógico y una teoría de conjuntos.
Aquí no hay distinción entre blanco y negro: muchos idiomas encajan entre ellos. Por ejemplo, el sistema de tipos del lenguaje Haskell tiene raíces en el trabajo de Russel, puede verse como un sistema simplificado de Agda, pero desde el punto de vista matemático, es inconsistente (autocontradictorio) si se ve como un sistema lógico o una teoría de conjuntos.
Sin embargo, como vehículo teórico para proteger los programas de Haskell de errores, funciona bastante bien. Incluso puede usar tipos para codificar ciertas propiedades y sus pruebas, pero no todas las propiedades pueden codificarse, y el programador aún puede violar las propiedades probadas si usa hacks sucios desalentados.
El sistema de tipos de Scala está aún más alejado del trabajo de Russel y del lenguaje de prueba perfecto de Agda, pero aún tiene raíces en el trabajo de Russel.
En cuanto a las propiedades de prueba de los lenguajes industriales cuyos sistemas de tipos no fueron diseñados para eso, existen muchos enfoques y sistemas.
Para enfoques interesantes pero diferentes, vea el proyecto de investigación Coq y Microsoft Boogie. Coq se basa en la teoría de tipos para generar programas imperativos a partir de programas Coq. Boogie se basa en la anotación de programas imperativos con propiedades y prueba de esas propiedades con el probador de teoremas Z3 utilizando un enfoque completamente diferente al de Coq.
Tienes razón sobre la motivación de Russell. Su paradoja plaga todas las teorías de conjuntos que admiten axiomas de comprensión irrestrictos en el sentido de que: cualquier función proposicional determina un conjunto, es decir, la de todas aquellas entidades que satisfacen la función. Entre las teorías basadas en conjuntos que tenían ese defecto estaban la ingenua teoría de conjuntos de Cantor y el sistema de Grundgesetze de Frege (específicamente: axioma 5).
Dado que los tipos se consideran tipos especiales de conjuntos, si no se tiene cuidado, una paradoja similar puede colarse en un sistema de tipos. Dicho esto, no conozco ningún sistema de tipos que haya sufrido tal destino. Solo puedo recordar los primeros intentos de Church de formular el cálculo lambda en los años 30, que resultó ser inconsistente (paradoja de Kleene-Rosser), pero que no se debió a tipos ni a la paradoja de Russell.
Actualización : Vea la respuesta de Philip para una respuesta real a su pregunta.
fuente
Como mencionas Python, la pregunta no es puramente teórica. Así que trato de dar una perspectiva más amplia sobre los tipos. Los tipos son cosas diferentes para diferentes personas. He recopilado al menos 5 nociones distintas (pero relacionadas) de tipos:
Los sistemas de tipos son sistemas lógicos y teorías de conjuntos.
Un sistema de tipos asocia un tipo con cada valor calculado. Al examinar el flujo de estos valores, un sistema de tipos intenta probar o garantizar que no se produzcan errores de tipo.
Tipo es una clasificación que identifica uno de varios tipos de datos, como valor real, entero o booleano, que determina los valores posibles para ese tipo; las operaciones que se pueden realizar en valores de ese tipo; el significado de los datos; y la forma en que se pueden almacenar valores de ese tipo
Los tipos de datos abstractos permiten la abstracción de datos en lenguajes de alto nivel. Los ADT a menudo se implementan como módulos: la interfaz del módulo declara los procedimientos que corresponden a las operaciones de ADT. Esta estrategia de ocultación de información permite cambiar la implementación del módulo sin perturbar los programas del cliente.
Las implementaciones de lenguaje de programación usan tipos de valores para elegir el almacenamiento que necesitan los valores y algoritmos para las operaciones en los valores.
Las citas son de Wikipedia, pero puedo proporcionar mejores referencias en caso de necesidad.
Los tipos 1 surgieron del trabajo de Russel, pero hoy no solo están protegidos de las paradojas: el lenguaje mecanografiado de la teoría de los tipos de homotopía es una nueva forma de codificar las matemáticas en un lenguaje formal, entendible por la máquina, y una nueva forma para que los humanos entiendan los fundamentos de las matematicas. (La forma "antigua" es codificar usando una teoría de conjuntos axiomática).
Los tipos 2-5 surgieron en la programación a partir de varias necesidades diferentes: evitar errores, clasificar los diseñadores de software de datos y los programadores con los que trabajan, diseñar sistemas grandes e implementar lenguajes de programación de manera eficiente, respectivamente.
Los sistemas de tipos en C / C ++, Ada, Java, Python no surgieron del trabajo de Russel o del deseo de evitar errores. Surgieron de la necesidad de describir diferentes tipos de datos (por ejemplo, "el apellido es una cadena de caracteres y no un número"), modularizar el diseño del software y elegir representaciones de bajo nivel para los datos de manera óptima. Estos idiomas no tienen tipos-1 o tipos-2. Java garantiza una seguridad relativa contra errores no mediante la prueba de la corrección del programa utilizando el sistema de tipos, sino mediante un diseño cuidadoso del lenguaje (sin aritmética de puntero) y el sistema de tiempo de ejecución (máquina virtual, verificación de código de bytes). El sistema de tipos en Java no es un sistema lógico ni una teoría de conjuntos.
Sin embargo, el sistema de tipos en el lenguaje de programación Agda es una variante moderna del sistema de tipos de Russel (basado en trabajos posteriores o de Per Martin-Lof y otros matemáticos). El sistema de tipos en Agda está diseñado para expresar las propiedades matemáticas del programa y las pruebas de esas propiedades, es un sistema lógico y una teoría de conjuntos.
Aquí no hay distinción entre blanco y negro: muchos idiomas encajan entre ellos. Por ejemplo, el sistema de tipos del lenguaje Haskell tiene raíces en el trabajo de Russel, puede verse como un sistema simplificado de Agda, pero desde el punto de vista matemático, es inconsistente (autocontradictorio) si se ve como un sistema lógico o una teoría de conjuntos.
Sin embargo, como vehículo teórico para proteger los programas de Haskell de errores, funciona bastante bien. Incluso puede usar tipos para codificar ciertas propiedades y sus pruebas, pero no todas las propiedades pueden codificarse, y el programador aún puede violar las propiedades probadas si usa hacks sucios desalentados.
El sistema de tipos de Scala está aún más alejado del trabajo de Russel y del lenguaje de prueba perfecto de Agda, pero aún tiene raíces en el trabajo de Russel.
En cuanto a las propiedades de prueba de los lenguajes industriales cuyos sistemas de tipos no fueron diseñados para eso, existen muchos enfoques y sistemas.
Para enfoques interesantes pero diferentes, vea el proyecto de investigación Coq y Microsoft Boogie. Coq se basa en la teoría de tipos para generar programas imperativos a partir de programas Coq. Boogie se basa en la anotación de programas imperativos con propiedades y prueba de esas propiedades con el probador de teoremas Z3 utilizando un enfoque completamente diferente al de Coq.
fuente