Abusar del álgebra de los tipos de datos algebraicos: ¿por qué funciona esto?

La expresión 'algebraica' para los tipos de datos algebraicos parece muy sugerente para alguien con experiencia en matemáticas. Déjame intentar explicar lo que quiero decir.

Habiendo definido los tipos básicos

• Producto •
• Unión +
• único X
• Unidad 1

y usando la taquigrafía X²para X•Xy 2Xpara X+Xetcétera, podemos definir expresiones algebraicas para, por ejemplo, listas vinculadas

data List a = Nil | Cons a (List a) ↔ L = 1 + X • L

y árboles binarios:

data Tree a = Nil | Branch a (Tree a) (Tree a) ↔ T = 1 + X • T²

Ahora, mi primer instinto como matemático es volverme loco con estas expresiones, y tratar de resolver por Ly T. Podría hacer esto mediante la sustitución repetida, pero parece mucho más fácil abusar de la notación horriblemente y pretender que puedo reorganizarla a voluntad. Por ejemplo, para una lista vinculada:

L = 1 + X • L

(1 - X) • L = 1

L = 1 / (1 - X) = 1 + X + X² + X³ + ...

donde he usado la expansión de la serie de potencia de 1 / (1 - X)una manera totalmente injustificada para obtener un resultado interesante, a saber, que un Ltipo es Nil, o contiene 1 elemento, o contiene 2 elementos, o 3, etc.

Se vuelve más interesante si lo hacemos para árboles binarios:

T = 1 + X • T²

X • T² - T + 1 = 0

T = (1 - √(1 - 4 • X)) / (2 • X)

T = 1 + X + 2 • X² + 5 • X³ + 14 • X⁴ + ...

nuevamente, usando la expansión de la serie de potencia (hecho con Wolfram Alpha ). Esto expresa el hecho no obvio (para mí) de que solo hay un árbol binario con 1 elemento, 2 árboles binarios con dos elementos (el segundo elemento puede estar en la rama izquierda o derecha), 5 árboles binarios con tres elementos, etc. .

Entonces mi pregunta es: ¿qué estoy haciendo aquí? Estas operaciones parecen injustificadas (¿cuál es exactamente la raíz cuadrada de un tipo de datos algebraicos de todos modos?) Pero conducen a resultados sensibles. ¿El cociente de dos tipos de datos algebraicos tiene algún significado en informática o es simplemente un truco de notación?

Y, quizás más interesante, ¿es posible extender estas ideas? ¿Existe una teoría del álgebra de tipos que permita, por ejemplo, funciones arbitrarias en los tipos, o los tipos requieren una representación en serie de potencia? Si puede definir una clase de funciones, ¿tiene algún significado la composición de funciones?

Descargo de responsabilidad: Mucho de esto realmente no funciona del todo bien cuando se tiene en cuenta ⊥, por lo que voy a ignorarlo descaradamente por razones de simplicidad.

Algunos puntos iniciales:

• Tenga en cuenta que "unión" probablemente no sea el mejor término para A + B aquí; esa es específicamente una unión disjunta de los dos tipos, porque los dos lados se distinguen incluso si sus tipos son los mismos. Para lo que vale, el término más común es simplemente "tipo de suma".

• Los tipos Singleton son, efectivamente, todos los tipos de unidades. Se comportan de manera idéntica bajo manipulaciones algebraicas y, lo que es más importante, la cantidad de información presente aún se conserva.

• Probablemente quieras un tipo cero también. Haskell proporciona eso como Void. No hay valores cuyo tipo sea cero, al igual que hay un valor cuyo tipo es uno.

Todavía falta una operación importante aquí, pero volveré a eso en un momento.

Como probablemente haya notado, Haskell tiende a tomar prestados conceptos de la teoría de categorías, y todo lo anterior tiene una interpretación muy directa como tal:

• Dados los objetos A y B en Hask , su producto A × B es el tipo único (hasta el isomorfismo) que permite dos proyecciones fst : A × B → A y snd : A × B → B, donde se le da cualquier tipo C y funciones f : C → A, g : C → B puede definir el emparejamiento f &&& g : C → A × B de modo que fst ∘ (f &&& g) = f e igualmente para g . La parametricidad garantiza automáticamente las propiedades universales y mi elección menos sutil de nombres debería darle la idea. El (&&&)operador se define en Control.Arrow, por cierto.

• El doble de lo anterior es el coproducto A + B con inyecciones inl : A → A + B e inr : B → A + B, donde se le da cualquier tipo C y funciones f : A → C, g : B → C, puede definir el copairing f ||| g : A + B → C de tal manera que se mantengan las equivalencias obvias. Nuevamente, la parametricidad garantiza la mayoría de las partes difíciles automáticamente. En este caso, las inyecciones estándar son simplemente Lefty Righty el copairing es la función either.

Muchas de las propiedades de los tipos de producto y suma pueden derivarse de lo anterior. Tenga en cuenta que cualquier tipo singleton es un objeto terminal de Hask y cualquier tipo vacío es un objeto inicial.

Volviendo a la operación faltante mencionada anteriormente, en una categoría cerrada cartesiana tiene objetos exponenciales que corresponden a las flechas de la categoría. Nuestras flechas son funciones, nuestros objetos son tipos con clase *, y el tipo de A -> Bhecho se comporta como B ^A en el contexto de la manipulación algebraica de tipos. Si no es obvio por qué esto debería ser válido, considere el tipo Bool -> A. Con solo dos entradas posibles, una función de ese tipo es isomorfa a dos valores de tipo A, es decir (A, A). Porque Maybe Bool -> Atenemos tres entradas posibles, y así sucesivamente. Además, observe que si reformulamos la definición de copairing anterior para usar la notación algebraica, obtenemos la identidad C ^A × C ^B = C^{A + B} .

En cuanto a por qué todo esto tiene sentido, y en particular por qué su uso de la expansión de la serie de potencia está justificado, tenga en cuenta que gran parte de lo anterior se refiere a los "habitantes" de un tipo (es decir, valores distintos que tienen ese tipo) en orden para demostrar el comportamiento algebraico. Para hacer explícita esa perspectiva:

• El tipo de producto (A, B)representa un valor de cada uno Ay B, tomado independientemente. Entonces, para cualquier valor fijo a :: A, hay un valor de tipo (A, B)para cada habitante de B. Por supuesto, este es el producto cartesiano, y el número de habitantes del tipo de producto es el producto del número de habitantes de los factores.

• El tipo de suma Either A Brepresenta un valor de cualquiera Ao B, con las ramas izquierda y derecha distinguidas. Como se mencionó anteriormente, esta es una unión disjunta, y el número de habitantes del tipo suma es la suma del número de habitantes de los sumandos.

• El tipo exponencial B -> Arepresenta una asignación de valores de tipo Ba valores de tipo A. Para cualquier argumento fijo b :: B, Ase le puede asignar cualquier valor de ; un valor de tipo B -> Aelige uno de esos mapeos para cada entrada, que es equivalente a un producto de tantas copias Acomo Bhabitantes, de ahí la exponenciación.

Si bien es tentador al principio tratar los tipos como conjuntos, eso en realidad no funciona muy bien en este contexto: tenemos una unión disjunta en lugar de la unión estándar de conjuntos, no hay una interpretación obvia de la intersección o muchas otras operaciones de conjuntos, y nosotros por lo general, no me importa la membresía establecida (dejando eso al verificador de tipos)

Por otro lado, las construcciones anteriores pasan mucho tiempo hablando de contar habitantes, y enumerar los posibles valores de un tipo es un concepto útil aquí. Eso nos lleva rápidamente a la combinatoria enumerativa , y si consulta el artículo de Wikipedia vinculado, encontrará que una de las primeras cosas que hace es definir "pares" y "uniones" exactamente en el mismo sentido que los tipos de productos y sumas. genera funciones , luego hace lo mismo para "secuencias" que son idénticas a las listas de Haskell usando exactamente la misma técnica que usted.

Editar: Ah, y aquí hay un bono rápido que creo que demuestra el punto de manera sorprendente. Usted mencionó en un comentario que para un tipo de árbol T = 1 + T^2puede derivar la identidad T^6 = 1, lo cual es claramente incorrecto. Sin embargo, T^7 = T se sostiene, y se puede construir directamente una biyección entre árboles y siete tuplas de árboles, cf. Andreas Blass "Siete árboles en uno" .

Edición × 2: sobre el tema de la construcción "derivada de un tipo" mencionado en otras respuestas, también puede disfrutar este artículo del mismo autor que se basa en la idea, incluidas las nociones de división y otras cosas interesantes.

Los árboles binarios se definen por la ecuación T=1+XT^2en el semired de tipos. Por construcción, T=(1-sqrt(1-4X))/(2X)se define por la misma ecuación en el semired de números complejos. Entonces, dado que estamos resolviendo la misma ecuación en la misma clase de estructura algebraica, en realidad no debería sorprendernos que veamos algunas similitudes.

El problema es que cuando razonamos acerca de los polinomios en el semisecado de números complejos, generalmente usamos el hecho de que los números complejos forman un anillo o incluso un campo, por lo que nos encontramos utilizando operaciones como la resta que no se aplican a semirrelaciones. Pero a menudo podemos eliminar sustracciones de nuestros argumentos si tenemos una regla que nos permite cancelar desde ambos lados de una ecuación. Este es el tipo de cosas probadas por Fiore y Leinster que muestran que muchos argumentos sobre los anillos se pueden transferir a semirremolques.

Esto significa que gran parte de su conocimiento matemático sobre los anillos se puede transferir de manera confiable a los tipos. Como resultado, algunos argumentos que involucran números complejos o series de poder (en el anillo de las series de poder formales) pueden trasladarse a los tipos de una manera completamente rigurosa.

Sin embargo, hay más en la historia que esto. Una cosa es demostrar que dos tipos son iguales (digamos) al mostrar que dos series de potencia son iguales. Pero también puede deducir información sobre los tipos inspeccionando los términos en la serie de potencia. No estoy seguro de cuál debería ser la declaración formal aquí. (Recomiendo Brent Yorgey papel de las especies combinatorias para un trabajo que está estrechamente relacionados, pero son especies no los mismos que los tipos).

Lo que me parece alucinante es que lo que has descubierto se puede extender al cálculo. Los teoremas sobre cálculo pueden transferirse a la semisección de tipos. De hecho, incluso los argumentos sobre diferencias finitas pueden transferirse y usted encuentra que los teoremas clásicos del análisis numérico tienen interpretaciones en la teoría de tipos.

¡Que te diviertas!

Parece que todo lo que estás haciendo es expandir la relación de recurrencia.

L = 1 + X • L
L = 1 + X • (1 + X • (1 + X • (1 + X • ...)))
  = 1 + X + X^2 + X^3 + X^4 ...

T = 1 + X • T^2
L = 1 + X • (1 + X • (1 + X • (1 + X • ...^2)^2)^2)^2
  = 1 + X + 2 • X^2 + 5 • X^3 + 14 • X^4 + ...

Y dado que las reglas para las operaciones en los tipos funcionan como las reglas para las operaciones aritméticas, puede usar medios algebraicos para ayudarlo a descubrir cómo expandir la relación de recurrencia (ya que no es obvio).

No tengo una respuesta completa, pero estas manipulaciones tienden a 'simplemente funcionar'. Un artículo relevante podría ser Objetos de categorías como números complejos de Fiore y Leinster . Me lo encontré mientras leía el blog de sigfpe sobre un tema relacionado ; ¡El resto de ese blog es una mina de oro para ideas similares y vale la pena echarle un vistazo!

También puede diferenciar los tipos de datos, por cierto, ¡eso le dará la Cremallera adecuada para el tipo de datos!

El álgebra de los procesos de comunicación (ACP) trata con tipos similares de expresiones para procesos. Ofrece suma y multiplicación como operadores de elección y secuencia, con elementos neutros asociados. En base a estos, hay operadores para otras construcciones, como el paralelismo y la interrupción. Ver http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes . También hay un artículo en línea llamado "Una breve historia del álgebra de procesos".

Estoy trabajando en extender lenguajes de programación con ACP. El pasado abril presenté un artículo de investigación en Scala Days 2012, disponible en http://code.google.com/p/subscript/

En la conferencia demostré un depurador que ejecuta una especificación recursiva paralela de una bolsa:

Bolsa = A; (Bolsa y a)

donde A y un soporte para acciones de entrada y salida; el punto y coma y el signo y representan secuencia y paralelismo. Vea el video en SkillsMatter, accesible desde el enlace anterior.

Una especificación de bolsa más comparable a

L = 1 + X • L

sería

B = 1 + X&B

ACP define paralelismo en términos de elección y secuencia utilizando axiomas; ver el artículo de Wikipedia. Me pregunto para qué sería la analogía del bolso

L = 1 / (1-X)

La programación de estilo ACP es útil para analizadores de texto y controladores GUI. Especificaciones como

searchCommand = hecho clic (searchButton) + tecla (Enter)

cancelCommand = hecho clic (cancelButton) + tecla (Escape)

puede escribirse de manera más concisa haciendo implícitos los dos refinamientos "cliqueados" y "clave" (como lo que Scala permite con funciones). Por eso podemos escribir:

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

El lado derecho ahora contiene operandos que son datos, en lugar de procesos. En este nivel, no es necesario saber qué refinamientos implícitos convertirán estos operandos en procesos; no necesariamente se refinarían en acciones de entrada; También se aplicarían acciones de salida, por ejemplo, en la especificación de un robot de prueba.

Los procesos obtienen así datos como compañeros; así acuño el término "álgebra de ítems".

Serie de cálculo y maclaurina con tipos

Aquí hay otra adición menor: una visión combinatoria de por qué los coeficientes en una expansión de serie deberían 'funcionar', en particular enfocándose en series que pueden derivarse usando el enfoque de Taylor-Maclaurin a partir del cálculo. NB: la expansión de serie de ejemplo que da del tipo de lista manipulada es una serie de Maclaurin.

Dado que otras respuestas y comentarios abordan el comportamiento de las expresiones de tipo algebraico (sumas, productos y exponentes), esta respuesta eludirá ese detalle y se centrará en el tipo 'cálculo'.

Puede notar comas invertidas haciendo un trabajo pesado en esta respuesta. Hay dos razones:

• estamos en el negocio de dar interpretaciones de un dominio a entidades de otro y parece apropiado delimitar tales nociones extranjeras de esta manera.
• algunas nociones podrán formalizarse de manera más rigurosa, pero la forma y las ideas parecen más importantes (y requieren menos espacio para escribir) que los detalles.

Definición de serie Maclaurin

La serie Maclaurin de una función f : ℝ → ℝse define como

f(0) + f'(0)X + (1/2)f''(0)X² + ... + (1/n!)f⁽ⁿ⁾(0)Xⁿ + ...

donde f⁽ⁿ⁾significa la nderivada th de f.

Para poder dar sentido a la serie de Maclaurin como interpretada con tipos, necesitamos entender cómo podemos interpretar tres cosas en un contexto de tipo:

• una derivada (posiblemente múltiple)
• aplicando una función a 0
• términos como (1/n!)

y resulta que estos conceptos del análisis tienen contrapartes adecuadas en el mundo tipo.

¿Qué quiero decir con "contraparte adecuada"? Debería tener el sabor de un isomorfismo: si podemos preservar la verdad en ambas direcciones, los hechos derivables en un contexto pueden transferirse al otro.

Cálculo con tipos

Entonces, ¿qué significa la derivada de una expresión de tipo? ¡Resulta que para una clase grande y bien comportada ('diferenciable') de expresiones de tipo y functores, hay una operación natural que se comporta de manera similar como para ser una interpretación adecuada!

Para estropear el remate, la operación análoga a la diferenciación es la de hacer 'contextos de un agujero'. Este es un excelente lugar para ampliar aún más este punto en particular, pero el concepto básico de un contexto de un agujero ( da/dx) es que representa el resultado de extraer un solo subpunto de un tipo particular ( x) de un término (de tipo a), preservando toda otra información, incluida la necesaria para determinar la ubicación original del subpunto. Por ejemplo, una forma de representar un contexto de un agujero para una lista es con dos listas: una para los elementos anteriores a la extraída y otra para los elementos posteriores.

La motivación para identificar esta operación con diferenciación proviene de las siguientes observaciones. Escribimos da/dxpara significar el tipo de contextos de un agujero para tipo acon agujero de tipo x.

d1/dx = 0
dx/dx = 1
d(a + b)/dx = da/dx + db/dx
d(a × b)/dx = a × db/dx + b × da/dx
d(g(f(x))/dx = d(g(y))/dy[f(x)/a] × df(x)/dx

Aquí, 1y 0representan tipos con exactamente uno y exactamente cero habitantes, respectivamente, +y ×representan tipos de suma y producto como de costumbre. fy gse usan para representar funciones de tipo, o formadores de expresión de tipo, y [f(x)/a]significa la operación de sustituir f(x)cada uno aen la expresión anterior.

Esto puede escribirse en un estilo sin puntos, escribiendo f'para significar la función derivada de la función de tipo f, por lo tanto:

(x ↦ 1)' = x ↦ 0
(x ↦ x)' = x ↦ 1
(f + g)' = f' + g'
(f × g)' = f × g' + g × f'
(g ∘ f)' = (g' ∘ f) × f'

que puede ser preferible

NB las igualdades pueden hacerse rigurosas y exactas si definimos derivadas usando clases de tipos y functores de isomorfismo.

Ahora, notamos en particular que las reglas de cálculo pertenecientes a las operaciones algebraicas de adición, multiplicación y composición (a menudo llamadas las reglas de Suma, Producto y Cadena) se reflejan exactamente por la operación de "hacer un agujero". Además, los casos básicos de 'hacer un agujero' en una expresión constante o el término en xsí también se comportan como diferenciación, por lo que por inducción obtenemos un comportamiento de diferenciación para todas las expresiones de tipo algebraico.

Ahora podemos interpretar la diferenciación, ¿qué significa la n'derivada' de una expresión tipo dⁿe/dxⁿ? Es un tipo que representa ncontextos de lugar: términos que, cuando se 'llenan' con ntérminos de tipo, xproducen un e. Hay otra observación clave relacionada con (1/n!)"venir más tarde".

La parte invariante de un tipo functor: aplicando una función a 0

Ya tenemos una interpretación para 0en el mundo tipográfico: un tipo vacío sin miembros. ¿Qué significa, desde un punto de vista combinatorio, aplicarle una función de tipo? En términos más concretos, suponiendo que fes una función de tipo, ¿cómo se f(0)ve? Bueno, ciertamente no tenemos acceso a nada de tipo 0, por lo que cualquier construcción f(x)que requiera un xno está disponible. Lo que queda son aquellos términos que son accesibles en su ausencia, que podemos llamar la parte 'invariante' o 'constante' del tipo.

Para un ejemplo explícito, tome el Maybefunctor, que se puede representar algebraicamente como x ↦ 1 + x. Cuando aplicamos esto a 0, obtenemos 1 + 0, es como 1: el único valor posible es el Nonevalor. Para una lista, de manera similar, obtenemos solo el término correspondiente a la lista vacía.

Cuando lo recuperamos e interpretamos el tipo f(0)como un número, se puede considerar como el recuento de cuántos términos de tipo f(x)(para cualquiera x) se pueden obtener sin acceso a un x: es decir, el número de términos "vacíos". .

Poniéndolo todo junto: interpretación completa de una serie de Maclaurin

Me temo que no puedo pensar en una interpretación directa apropiada de (1/n!)un tipo.

Si tenemos en cuenta, sin embargo, el tipo f⁽ⁿ⁾(0)a la luz de lo anterior, vemos que se puede interpretar como el tipo de ncontextos -Ponga por un término de tipo de f(x)los que aún no tienen un x - es decir, cuando nos integramos '' a nveces , el término resultante tiene exactamente n x s, ni más ni menos. Entonces, la interpretación del tipo f⁽ⁿ⁾(0)como un número (como en los coeficientes de la serie de Maclaurin de f) es simplemente un recuento de cuántos ncontextos de lugares vacíos existen. ¡Ya casi llegamos!

¿Pero dónde (1/n!)termina? Examinar el proceso de tipo 'diferenciación' nos muestra que, cuando se aplica varias veces, conserva el 'orden' en el que se extraen los subterms. Por ejemplo, considere el término (x₀, x₁)de tipo x × xy la operación de 'hacer un agujero' en él dos veces. Obtenemos ambas secuencias

(x₀, x₁)  ↝  (_₀, x₁)  ↝  (_₀, _₁)
(x₀, x₁)  ↝  (x₀, _₀)  ↝  (_₁, _₀)
(where _ represents a 'hole')

aunque ambos provienen del mismo término, porque hay 2! = 2formas de tomar dos elementos de dos, preservando el orden. En general, hayn! formas de tomar nelementos de n. Entonces, para obtener un recuento del número de configuraciones de un tipo de functor que tienen nelementos, tenemos que contar el tipo f⁽ⁿ⁾(0)y dividir por n!, exactamente como en los coeficientes de la serie Maclaurin.

Por lo tanto, dividir por n!resulta ser interpretable simplemente como sí mismo.

Reflexiones finales: definiciones 'recursivas' y analiticidad

Primero, algunas observaciones:

• si una función f: ℝ → ℝ tiene una derivada, esta derivada es única
• de manera similar, si una función f: ℝ → ℝ es analítica, tiene exactamente una serie polinómica correspondiente

Como tenemos la regla de la cadena, podemos usar la diferenciación implícita si formalizamos derivadas de tipo como clases de isomorfismo. ¡Pero la diferenciación implícita no requiere maniobras alienígenas como la resta o la división! Entonces podemos usarlo para analizar definiciones de tipo recursivo. Para tomar su ejemplo de lista, tenemos

L(X) ≅ 1 + X × L(X)
L'(X) = X × L'(X) + L(X)

y luego podemos evaluar

L'(0) = L(0) = 1

para obtener el coeficiente de X¹en la serie Maclaurin.

Pero dado que confiamos en que estas expresiones son estrictamente 'diferenciables', aunque solo sea implícitamente, y dado que tenemos la correspondencia con las funciones ℝ → ℝ, donde las derivadas son ciertamente únicas, podemos estar seguros de que incluso si obtenemos los valores usando ' operaciones ilegales, el resultado es válido.

Ahora, de manera similar, para usar la segunda observación, debido a la correspondencia (¿es un homomorfismo?) Con las funciones ℝ → ℝ, lo sabemos, siempre que estemos satisfechos de que una función tenga una serie de Maclaurin, si podemos encontrar alguna serie en todos , los principios descritos anteriormente se pueden aplicar para hacerlo riguroso.

En cuanto a su pregunta sobre la composición de funciones, supongo que la regla de la cadena proporciona una respuesta parcial.

No estoy seguro de a cuántos ADT de estilo Haskell se aplica esto, pero sospecho que son muchos, si no todos. He descubierto una prueba realmente maravillosa de este hecho, pero este margen es demasiado pequeño para contenerlo ...

Ahora, ciertamente esta es solo una forma de resolver lo que está sucediendo aquí y probablemente hay muchas otras formas.

Resumen: TL; DR

• el tipo 'diferenciación' corresponde a ' hacer un agujero '.
• aplicando un functor para 0obtener los términos "vacíos" para ese functor.
• Las series de potencia de Maclaurin , por lo tanto (algo) corresponden rigurosamente a la enumeración del número de miembros de un tipo de functor con un cierto número de elementos.
• La diferenciación implícita hace que esto sea más hermético.
• La singularidad de los derivados y la singularidad de las series de potencia significa que podemos evitar los detalles y funciona.

Teoría de tipo dependiente y funciones de tipo 'arbitrarias'

Mi primera respuesta a esta pregunta fue alta en conceptos y baja en detalles y se reflejó en la pregunta previa, "¿qué está pasando?"; esta respuesta será la misma pero centrada en la pregunta secundaria, "¿podemos obtener funciones de tipo arbitrarias?".

Una extensión de las operaciones algebraicas de suma y producto son los llamados 'operadores grandes', que representan la suma y el producto de una secuencia (o más generalmente, la suma y el producto de una función sobre un dominio) generalmente escritos Σy Πrespectivamente. Ver notación Sigma .

Entonces la suma

a₀ + a₁X + a₂X² + ...

podría estar escrito

Σ[i ∈ ℕ]aᵢXⁱ

donde ahay alguna secuencia de números reales, por ejemplo. El producto se representaría de manera similar con en Πlugar de Σ.

Cuando miras desde la distancia, este tipo de expresión se parece mucho a una función 'arbitraria' en X; Por supuesto, estamos limitados a series expresables y sus funciones analíticas asociadas. ¿Es este un candidato para una representación en una teoría de tipos? ¡Seguro!

La clase de teorías de tipos que tienen representaciones inmediatas de estas expresiones es la clase de teorías de tipos 'dependientes': teorías con tipos dependientes. Naturalmente, tenemos términos que dependen de términos, y en lenguajes como Haskell con funciones de tipo y cuantificación de tipo, términos y tipos dependiendo de los tipos. En un entorno dependiente, también tenemos tipos según los términos. Haskell no es un lenguaje de tipo dependiente, aunque muchas características de los tipos dependientes se pueden simular torturando un poco el idioma .

Curry-Howard y tipos dependientes

El 'isomorfismo de Curry-Howard' comenzó como una observación de que los términos y las reglas de cálculo de tipo del cálculo lambda de tipo simple corresponden exactamente a la deducción natural (según lo formulado por Gentzen) aplicada a la lógica proposicional intuitiva, con tipos que reemplazan las proposiciones. y términos que reemplazan a las pruebas, a pesar de que los dos se inventaron / descubrieron de forma independiente. Desde entonces, ha sido una gran fuente de inspiración para los teóricos de tipos. Una de las cosas más obvias a considerar es si, y cómo, esta correspondencia para la lógica proposicional puede extenderse a lógicas predicadas o de orden superior. Las teorías de tipo dependiente surgieron inicialmente de esta vía de exploración.

Para obtener una introducción al isomorfismo de Curry-Howard para el cálculo lambda de tipo simple, consulte aquí . Como ejemplo, si queremos probar A ∧ Bdebemos probar Ay probar B; Una prueba combinada es simplemente un par de pruebas: una para cada conjunto.

En deducción natural:

Γ ⊢ A    Γ ⊢ B
Γ ⊢ A ∧ B

y en cálculo lambda de tipo simple:

Γ ⊢ a : A    Γ ⊢ b : B
Γ ⊢ (a, b) : A × B

Existen correspondencias similares para los ∨tipos de suma, los →tipos de función y las diversas reglas de eliminación.

Una proposición no demostrable (intuitivamente falsa) corresponde a un tipo deshabitado.

Con la analogía de los tipos como proposiciones lógicas en mente, podemos comenzar a considerar cómo modelar predicados en el mundo tipográfico. Hay muchas formas en que esto se ha formalizado (consulte esta introducción a la teoría de tipo intuitiva de Martin-Löf para un estándar ampliamente utilizado) pero el enfoque abstracto generalmente observa que un predicado es como una proposición con variables de término libre, o, alternativamente, una función que toma términos para proposiciones. Si permitimos que las expresiones de tipo contengan términos, ¡un tratamiento en estilo de cálculo lambda se presenta inmediatamente como una posibilidad!

Considerando solo las pruebas constructivas, ¿de qué constituye una prueba ∀x ∈ X.P(x)? Podemos considerarlo como una función de prueba, tomando términos ( x) a pruebas de sus proposiciones correspondientes ( P(x)). Así que los miembros (pruebas) del tipo (proposición) ∀x : X.P(x)son funciones dependientes '', que para cada xen Xdar un término de tipo P(x).

¿Qué hay de ∃x ∈ X.P(x)? Tenemos que cualquier miembro de X, xjunto con una prueba de P(x). Por lo tanto, los miembros (pruebas) del tipo (proposición) ∃x : X.P(x)son 'pares dependientes': un término distinguido xen X, junto con un término de tipo P(x).

Notación: usaré

∀x ∈ X...

para declaraciones reales sobre miembros de la clase X, y

∀x : X...

para expresiones de tipo correspondientes a la cuantificación universal sobre tipo X. Del mismo modo para ∃.

Consideraciones combinatorias: productos y sumas

Además de la correspondencia Curry-Howard de tipos con proposiciones, tenemos la correspondencia combinatoria de tipos algebraicos con números y funciones, que es el punto principal de esta pregunta. Afortunadamente, esto se puede extender a los tipos dependientes descritos anteriormente.

Usaré la notación de módulo

|A|

para representar el "tamaño" de un tipo A, para hacer explícita la correspondencia descrita en la pregunta, entre tipos y números. Tenga en cuenta que este es un concepto fuera de la teoría; No afirmo que sea necesario que exista un operador de este tipo dentro del idioma.

Cuentemos los posibles miembros de tipo (totalmente reducidos, canónicos)

∀x : X.P(x)

cuál es el tipo de funciones dependientes que toman términos xde tipo Xa términos de tipo P(x). Cada una de esas funciones debe tener una salida para cada término de X, y esta salida debe ser de un tipo particular. Para cada uno xde X, a continuación, esto da |P(x)|'opciones' de salida.

El remate es

|∀x : X.P(x)| = Π[x : X]|P(x)|

lo cual, por supuesto, no tiene mucho sentido si lo Xes IO (), pero es aplicable a los tipos algebraicos.

Del mismo modo, un término de tipo

∃x : X.P(x)

es el tipo de pares (x, p)con p : P(x), así que dado cualquiera xde ellos Xpodemos construir un par apropiado con cualquier miembro de P(x), dando |P(x)|'opciones'.

Por lo tanto,

|∃x : X.P(x)| = Σ[x : X]|P(x)|

con las mismas advertencias.

Esto justifica la notación común para los tipos dependientes en las teorías que usan los símbolos Πy Σ, de hecho, muchas teorías desdibujan la distinción entre 'para todos' y 'producto' y entre 'hay' y 'suma', debido a las correspondencias mencionadas anteriormente.

Nos estamos acercando!

Vectores: representando tuplas dependientes

¿Podemos ahora codificar expresiones numéricas como

Σ[n ∈ ℕ]Xⁿ

como expresiones de tipo?

No exactamente. Si bien podemos considerar informalmente el significado de expresiones como Xⁿen Haskell, donde Xes un tipo y nun número natural, es un abuso de notación; esto es una expresión de tipo que contiene un número: claramente no una expresión válida.

Por otro lado, con tipos dependientes en la imagen, los tipos que contienen números son precisamente el punto; de hecho, las tuplas dependientes o 'vectores' son un ejemplo muy citado de cómo los tipos dependientes pueden proporcionar seguridad pragmática a nivel de tipo para operaciones como el acceso a listas . Un vector es solo una lista junto con información de nivel de tipo con respecto a su longitud: precisamente lo que buscamos para expresiones de tipo como Xⁿ.

Mientras dure esta respuesta, dejemos

Vec X n

ser el tipo de longitud- nvectores de Xvalores de tipo.

Técnicamente naquí hay, en lugar de un número natural real , una representación en el sistema de un número natural. Podemos representar números naturales ( Nat) en el estilo de Peano como cero ( 0) o el sucesor ( S) de otro número natural, y para que n ∈ ℕyo escriba ˻n˼signifique el término en el Natque representa n. Por ejemplo, ˻3˼es S (S (S 0)).

Entonces nosotros tenemos

|Vec X ˻n˼| = |X|ⁿ

para cualquier n ∈ ℕ.

Tipos nat: promoviendo ℕ términos a tipos

Ahora podemos codificar expresiones como

Σ[n ∈ ℕ]Xⁿ

como tipos Esta expresión particular daría lugar a un tipo que, por supuesto, es isomorfo al tipo de listas de X, como se identifica en la pregunta. (No solo eso, sino desde un punto de vista teórico de categoría, la función de tipo, que es un functor, que lleva Xal tipo anterior es naturalmente isomorfa para el functor de Lista).

Una pieza final del rompecabezas para las funciones 'arbitrarias' es cómo codificar, para

f : ℕ → ℕ

expresiones como

Σ[n ∈ ℕ]f(n)Xⁿ

para que podamos aplicar coeficientes arbitrarios a una serie de potencias.

Ya entendemos la correspondencia de los tipos algebraicos con los números, lo que nos permite mapear de tipos a números y funciones de tipo a funciones numéricas. ¡También podemos ir hacia otro lado! - tomando un número natural, obviamente hay un tipo algebraico definible con tantos miembros de término, tengamos o no tipos dependientes. Podemos probar esto fácilmente fuera de la teoría de tipos por inducción. Lo que necesitamos es una forma de mapear de números naturales a tipos, dentro del sistema.

Una comprensión agradable es que, una vez que tenemos tipos dependientes, la prueba por inducción y la construcción por recursividad se vuelven íntimamente similares; de hecho, son lo mismo en muchas teorías. Como podemos probar por inducción que existen tipos que satisfacen nuestras necesidades, ¿no deberíamos ser capaces de construirlos?

Hay varias formas de representar tipos a nivel de término. Usaré aquí una notación imaginaria de Haskellish *para el universo de tipos, generalmente considerada un tipo en un entorno dependiente. ¹

Del mismo modo, también hay al menos tantas formas de anotar la " ℕeliminación" como las teorías de tipos dependientes. Usaré una notación de coincidencia de patrones Haskellish.

Necesitamos un mapeo, αdesde Nathasta *, con la propiedad

∀n ∈ ℕ.|α ˻n˼| = n.

La siguiente pseudodefinición es suficiente.

data Zero -- empty type
data Successor a = Z | Suc a -- Successor ≅ Maybe

α : Nat -> *
α 0 = Zero
α (S n) = Successor (α n)

Entonces vemos que la acción de αrefleja el comportamiento del sucesor S, convirtiéndolo en una especie de homomorfismo. Successores una función de tipo que 'agrega uno' al número de miembros de un tipo; es decir, |Successor a| = 1 + |a|para cualquiera acon un tamaño definido.

Por ejemplo α ˻4˼(que es α (S (S (S (S 0))))), es

Successor (Successor (Successor (Successor Zero)))

y los términos de este tipo son

Z
Suc Z
Suc (Suc Z)
Suc (Suc (Suc Z))

que nos da exactamente cuatro elementos: |α ˻4˼| = 4.

Asimismo, para cualquiera n ∈ ℕ, tenemos

|α ˻n˼| = n

según sea necesario.

1. Muchas teorías requieren que los miembros *sean meros representantes de tipos, y una operación se proporciona como un mapeo explícito de términos de tipo *a sus tipos asociados. Otras teorías permiten que los tipos literales sean entidades de nivel de término.

¿Funciones 'arbitrarias'?

¡Ahora tenemos el aparato para expresar una serie de potencias totalmente generales como un tipo!

Las series

Σ[n ∈ ℕ]f(n)Xⁿ

se convierte en el tipo

∃n : Nat.α (˻f˼ n) × (Vec X n)

donde ˻f˼ : Nat → Nathay alguna representación adecuada dentro del lenguaje de la función f. Podemos ver esto de la siguiente manera.

|∃n : Nat.α (˻f˼ n) × (Vec X n)|
    = Σ[n : Nat]|α (˻f˼ n) × (Vec X n)|          (property of ∃ types)
    = Σ[n ∈ ℕ]|α (˻f˼ ˻n˼) × (Vec X ˻n˼)|        (switching Nat for ℕ)
    = Σ[n ∈ ℕ]|α ˻f(n)˼ × (Vec X ˻n˼)|           (applying ˻f˼ to ˻n˼)
    = Σ[n ∈ ℕ]|α ˻f(n)˼||Vec X ˻n˼|              (splitting product)
    = Σ[n ∈ ℕ]f(n)|X|ⁿ                           (properties of α and Vec)

¿Qué tan 'arbitrario' es esto? Estamos limitados no solo a los coeficientes enteros por este método, sino a los números naturales. Aparte de eso, fpuede ser cualquier cosa, dado un lenguaje Turing Complete con tipos dependientes, podemos representar cualquier función analítica con coeficientes numéricos naturales.

No he investigado la interacción de esto con, por ejemplo, el caso provisto en la pregunta de List X ≅ 1/(1 - X)o qué posible sentido podrían tener estos 'tipos' negativos y no enteros en este contexto.

Esperemos que esta respuesta sirva para explorar hasta dónde podemos llegar con las funciones de tipo arbitrario.