Introducción a los conceptos avanzados de Tauchain
Hace poco traducí un artículo publicado en el blog de Tauchain donde se explicaban los conceptos avanzados de la iniciativa, pero pudo resultar bastante complejo de entender para alguien que no está iniciado en arquitectura de la información. El artículo a continuación es una traducción de este, publicado por el usuario @dana-edwars en el que se explican los conceptos básicos de una forma más introductoria.
Conceptos avanzados de Tauchain
Esta es una introudcción a algunos de los más avanzados conceptos de Tauchain. Conceptos los cuales estructuran la fundación de Tauchain como un trinitarismo computacional que incluy proposiciones como tipos, programas como pruebas, y la relación entre teoría de tipos y teoría de categorías.
Proposiciones como tipos
La mayoría de programadores tienen una idea de que son los tipos. Por ejemplo en C/C++ tienes tipos como int (entero) char (carácter) y float (decimal). Mediante el uso de los tipos en C++ una persona puede hacer algo básico como esto:
#include <iostream>
using namespace std;
int main()
{
int a, b;
cin >> a >> b;
cout << a + b << endl;
}
En este rudimentario ejemplo tenemos un programa en C++ el cual suma tomando entradas, usando cin para pasar las variables a y b, y entonces un simple a+b los suma entre sí. Aquí el punto importante es que int es el tipo para entero.
Los lenguajes de programación tienen sistemas de tipos. El sistema de C++ es usado porque es un lenguaje muy familiar pero todos los lenguajes tienen sistemas de tipos. Las matemáticas detrás del sistema de tipos es llamada teoría de tipos y en particular Tauchain usa una modernísima teoría de tipos llamada teoría intuicionista de tipos. Una alternativa a la teoría intuicionista de tipos es llamada el cálculo lambda.
Los tipos en una teoría de tipos permitn la ausencia de paradojas para su uso en lógica formal. Lo que debe ser observado es que el isomorfismo Curry-Howard revela que los programas de ordenador son pruebas matemáticas.
Simplemente los lenguajes funcionales de programación como Adga garantzan que siempre terminan resolviendo completamente el problema de la interrupción del programa. Tauchain específicamente utliza tipos dependientes y esto tiene mayores beneficios cuando te das cuenta de la importancia de la seguridad de tipos y el comprobación de tipos.
Los tipos dependientes dependen de valores. En Adga, que es un ejemplo de un lenguaje de tipos dependientes funcional, puedes incuir valores dentro de tipos. La dependencia de tipos es una dependencia de vaor. Para dar un ejemplo de una dependencia de tipos que todo el mundo pueda entender usaré un ejemlo en lenguaje natural.
En lenguaje natural tenemos un concepto llamado meses. Los meses contienen días y son un grupo de días. La cantidad de días en un mes varía de año a año y de mes a mes. Los días pueden ser considerados un tipo de datos. Para cualquier mes m, hay un tipo (o conjunto) D(m). D(m) de los días en ese mes.
Así que para cualquier mes m, tenemos un tipo D(m). Por supuesto esto es un ejemplo extremadamente simplificado porque no todos los meses tienen el mismo número de días, pero en general un mes es un conjunto de días y el tipo D es un ejemplo de tipo de información para los días. D es un tipo que depende del mes y del año porque diferentes meses tienen diferente cantidad de días y tambien existen años bisiestos. Cualquier familia de conjuntos indexados por otro conjunto es un tipo dependiente y estos están por todas partes si miras cuidadosamente.
Programas como pruebas
Una prueba por construcción es también llamada una prueba constructiva. Esta contrasta con las pruebas existenciales por demostrar la existencia de un objeto matemático. La prueba de una preposición es una sentencia. Un programa como una prueba revela que la lógica y la programación son isomórfismos. Si estás haciendo programación estás haciendo lógica. En Tauchain estás capacitado para tomar ventaja del isomorfismo Curry-Howard y la teoría de tipos intuicionista para trabajar con todas las formas de conocimiento y hacer matemáticas.
La teoría de tipos intuicionista de Martin Lof es la fundación del compilador Tau. Tau será totalmente compatible con esto cuando este completado, lo cual permitirá al programador tener todos los fantásticos beneficios provistos por la teoría de tipos intuicionista de Martin Lof. (Nota del traductor: el equipo de Tau dejó comunicado hace un mes que esta teoría no es suficiente, podéis ver por qué en el anterior post)
La teoría de tipos homotópica es una idea relacionada que puede alcanzar una convergencia con Tauchain.
La relación entre teoría de tipos y teoría de categorías
Existen correspondencias entre teoría de tipos y teoría de categorías. Una categoría extrictamente cartesiana corresponde, por ejemplo, a la teoría de tipos de Martin Lof y al cálculo de tipos lambda. Esas relaciones van un poco más profundo que esto pero no iré tan profundo porque mis conocimientos de base no son matemáticos. Al mismo tiempo, quizás se puede decir que si eres un programador entonces eres un matemático y eso alude a la fundación de esas correspondencias.
La teoría de categorías funciona en muchos componentes. En particular una categoría es una estructura matemática como un grupo de un vector espacial definido abstractamente por axiomas, y en teoría de categorías hay un concepto llamado morfismos. Un morfimso es un mapa de preservación de la estructura de una estructura matemática a otra. Por ejemplo, una función es considerado un morfismo.
Simplificación de pruebas como evaluación de programas
¿Como evaluar cómo funcionará un programa antes de ejecutarlo? En Tau puedes razonar sobre el código y evaluarlo para una prueba de correción. Lenguajes como Adga usan tipos dependientes los cuales son tipos que dependen de valores o declaraciones. Podrá ser discutido más adelante sobre esto.
Conclusión
Espero haber proveído una introducción a algunos de los conceptos detrás de Tauchain. El trinitarismo computacional se basa en preposiciones como tipos, programas como pruebas y la relación entre teoría de tipos y teoría de categorías. El isomorfismo de Curry-Howard es lo que hace posible al trinitarismo computacional revelando que la programación es lógica.