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

La expresión ‘algebraica’ para los tipos de datos algebraicos parece muy sugestiva para alguien con una formación en matemáticas. Déjame intentar explicar lo que quiero decir.

Habiendo definido los tipos básicos

  • Producto
  • Unión +
  • Singleton X
  • Unidad 1

y usando la abreviatura para X•X y 2X para X+X , etc., podemos definir expresiones algebraicas para, por ejemplo, listas vinculadas

data List a = Nil | Cons a (List a) 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) 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 para L y T Podría hacer esto mediante una 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) de una manera totalmente injustificada para obtener un resultado interesante, a saber, que un tipo L 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⁴ + ...

de nuevo, usando la expansión de la serie de potencia (hecha 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 twig 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 razonables. ¿el cociente de dos tipos de datos algebraicos tiene algún significado en informática, o es solo un truco de notación?

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

Descargo de responsabilidad: Mucho de esto no funciona del todo bien cuando cuentas por ⊥, así que descarto descaradamente eso por simplicidad.

Algunos puntos iniciales:

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

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

  • Probablemente también quieras un tipo cero. No hay uno estándar, pero el nombre más común es Void . No hay valores cuyo tipo sea cero, del mismo modo 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 hayas notado, Haskell tiende a tomar prestados conceptos de la Teoría de Categoría, 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 da cualquier tipo C y funciones f : C → A, g : C → B se puede definir el emparejamiento f &&& g : C → A × B tal que fst ∘ (f &&& g) = f y del mismo modo para g . La parametricidad garantiza automáticamente las propiedades universales y mi selección de nombres no tan sutiles debería darte 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 defina el copaje f

g : A + B → C tal que las equivalencias obvias se mantienen. Nuevamente, la parametricidad garantiza la mayoría de las partes difíciles automáticamente. En este caso, las inyecciones estándar son simplemente Left y Right y el copairing es la función either .

Muchas de las propiedades de los tipos de producto y sum se pueden derivar 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 antes mencionada, en una categoría cerrada cartesiana tiene objetos exponenciales que corresponden a flechas de la categoría. Nuestras flechas son funciones, nuestros objetos son tipos con tipo * , y el tipo A -> B hecho se comporta como B A en el contexto de la manipulación algebraica de tipos. Si no es obvio por qué esto debería mantenerse, considere el tipo Bool -> A Con solo dos entradas posibles, una función de ese tipo es isomórfica para dos valores de tipo A , es decir (A, A) . Para Maybe Bool -> A tenemos tres entradas posibles, y así sucesivamente. Además, observe que si reformulamos la definición de copaocución 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é se justifica el uso de la expansión de la serie de potencias, 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 que esa perspectiva sea explícita:

  • El tipo de producto (A, B) representa un valor de A y B , tomado independientemente. Entonces, para cualquier valor fijo a :: A , hay un valor de tipo (A, B) para cada habitante de B Este es, por supuesto, 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 sum Either AB representa un valor de A o B , con las twigs izquierda y derecha distinguidas. Como se mencionó anteriormente, esta es una unión disjunta, y el número de habitantes del tipo sum es la sum del número de habitantes de los sumndos.

  • El tipo exponencial B -> A representa un mapeo de valores de tipo B a valores de tipo A Para cualquier argumento fijo b :: B , se le puede asignar cualquier valor de A ; un valor de tipo B -> A elige uno de esos mapeos para cada entrada, que es equivalente a un producto de tantas copias de A como B tiene habitantes, 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 intersección u otras operaciones de conjunto, y generalmente no me importa la membresía establecida (dejándola 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 enlazado de Wikipedia, encontrará que una de las primeras cosas que hace es definir “pares” y “uniones” exactamente en el mismo sentido que los tipos de producto y sum a través de generando funciones , luego hace lo mismo con las “secuencias” que son idénticas a las listas de Haskell utilizando exactamente la misma técnica que tú.


Edit: Ah, y aquí hay una bonificación rápida que creo que demuestra el punto llamativamente. Mencionaste en un comentario que para un árbol tipo T = 1 + T^2 puedes derivar la identidad T^6 = 1 , lo cual es claramente incorrecto. Sin embargo, T^7 = T se mantiene, y se puede construir directamente una biyección entre árboles y siete tuplas de árboles, cf. “Seven Trees in One” de Andreas Blass .

Edit × 2: sobre el tema de la construcción “derivada de un tipo” mencionado en otras respuestas, también puede disfrutar de este trabajo del mismo autor que se basa en la idea más allá, incluyendo nociones de división y otras cosas interesantes.

Los árboles binarios se definen por la ecuación T=1+XT^2 en el semiring de tipos. Por construcción, T=(1-sqrt(1-4X))/(2X) se define por la misma ecuación en el semicurado 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 sorprender que veamos algunas similitudes.

El problema es que cuando razonamos acerca de los polinomios en el semiencognición de números complejos usamos típicamente el hecho de que los números complejos forman un anillo o incluso un campo, por lo que nos encontramos utilizando operaciones tales como la resta que no se aplican a las semirredes. 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 cosa probada por Fiore y Leinster que muestra que muchos argumentos sobre anillos se pueden transferir a semirremolques.

Esto significa que muchos de sus conocimientos matemáticos sobre los anillos se pueden transferir de manera confiable a los tipos. Como resultado, algunos argumentos que involucran números complejos o series de poder (en el anillo de 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 probar que dos tipos son iguales (por ejemplo) mostrando que dos series de potencias son iguales. Pero también puede deducir información sobre tipos inspeccionando los términos en la serie de potencias. No estoy seguro de cuál debería ser la statement formal aquí. (Recomiendo el artículo de Brent Yorgey sobre especies combinatorias para algún trabajo que esté estrechamente relacionado, pero las especies no son lo mismo que los tipos).

Lo que me parece increíble es que lo que has descubierto se puede extender al cálculo. Los teoremas sobre el cálculo se pueden transferir al semired de tipos. De hecho, incluso los argumentos sobre las diferencias finitas se pueden transferir y se 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 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 ‘solo funcionar’. Un documento relevante podría ser Objetos de categorías como Números complejos de Fiore y Leinster . Lo encontré leyendo el blog de sigfpe sobre un tema relacionado ; el rest de ese blog es una mina de oro para ideas similares y vale la pena echarle un vistazo!

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

El Álgebra de Procesos de Comunicación (ACP) trata con tipos similares de expresiones para procesos. Ofrece la adición y la multiplicación como operadores de elección y secuencia, con elementos neutros asociados. En base a esto, existen operadores para otras construcciones, como paralelismo e interrupción. Ver http://en.wikipedia.org/wiki/Algebra_of_Communicating_Processes . También hay un documento en línea llamado “Una breve historia del proceso de álgebra”.

Estoy trabajando para extender los lenguajes de progtwigción con ACP. El pasado mes de abril presenté un trabajo de investigación en Scala Days 2012, disponible en http://code.google.com/p/subscript/

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

Bolsa = A; (Bolsa y a)

donde A y a representan las acciones de entrada y salida; el punto y coma y el signo & representan la secuencia y el 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 el paralelismo en términos de elección y secuencia usando axiomas; ver el artículo de Wikipedia. Me pregunto para qué sería la analogía de la bolsa

L = 1 / (1-X)

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

searchCommand = clicked (searchButton) + tecla (Intro)

cancelCommand = clicked (cancelButton) + tecla (Escape)

puede escribirse de forma más concisa haciendo que los dos refinamientos sean “cliqueados” y “clave” implícitamente (como lo que Scala permite con las funciones). Por lo tanto, podemos escribir:

searchCommand = searchButton + Enter

cancelCommand = cancelButton + Escape

Los lados derechos ahora contienen 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 refinarían en acciones de entrada; las acciones de salida también se aplicarían, por ejemplo, en la especificación de un robot de prueba.

Los procesos obtienen así los datos como acompañantes; así acuño el término “álgebra del artículo”.

Serie Cálculo y Maclaurin con tipos

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

Dado que otras respuestas y comentarios se relacionan con el comportamiento de expresiones de tipo algebraico (sums, productos y exponentes), esta respuesta eludirá ese detalle y se enfocará en el tipo ‘cálculo’.

Puedes notar que las comillas invertidas hacen algo 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 se podrán formalizar de manera más rigurosa, pero la forma y las ideas parecen más importantes (y ocupan menos espacio para escribir) que los detalles.

Definición de la 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 enésima derivada de f .

Para poder dar sentido a la serie de Maclaurin tal como se interpreta con los tipos, debemos comprender cómo podemos interpretar tres cosas en un contexto tipo:

  • un derivado (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 una “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 de buen comportamiento (‘diferenciable’) de expresiones de tipo y funtores, hay una operación natural que se comporta de manera similar para ser una interpretación adecuada.

Para estropear la frase final, la operación análoga a la diferenciación es la de hacer ‘contextos de un agujero’. Este es un excelente lugar para expandir aún más este punto particular, pero el concepto básico de un contexto de un agujero ( da/dx ) es que representa el resultado de extraer un único subelemento de un tipo particular ( x ) de un término (de escriba a ), conservando toda la demás información, incluida la necesaria para determinar la ubicación original del subelemento. Por ejemplo, una forma de representar un contexto de un agujero para una lista es con dos listas: una para los artículos que venían antes de la extraída y otra para los artículos que vinieron después.

La motivación para identificar esta operación con diferenciación proviene de las siguientes observaciones. Escribimos da/dx para indicar el tipo de contextos de un agujero para el tipo a con orificio 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í, 1 y 0 representan tipos con exactamente uno y exactamente cero habitantes, respectivamente, y + y × representan la sum y los tipos de producto como de costumbre. f y g se usan para representar funciones de tipo, o escribir formadores de expresión, y [f(x)/a] significa la operación de sustituir f(x) por cada a en la expresión precedente.

Esto se puede escribir en un estilo libre de 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 se pueden hacer rigurosas y exactas si definimos derivados utilizando clases de isomorfismos de tipos y funtores.

Ahora, notamos en particular que las reglas en cálculo pertenecientes a las operaciones algebraicas de sum, multiplicación y composición (a menudo llamadas reglas de sum, producto y cadena) se reflejan exactamente en la operación de “hacer un agujero”. Además, los casos base de ‘hacer un agujero’ en una expresión constante o el término x mismo también se comportan como diferenciación, de modo que por inducción obtenemos un comportamiento similar a la diferenciación para todas las expresiones de tipo algebraico.

Ahora podemos interpretar la diferenciación, ¿qué significa la n th ‘derivada’ de una expresión de tipo, dⁿe/dxⁿ ? Es un tipo que representa contextos n place: términos que, cuando se ‘llenan’ con n términos de tipo x producen una e . Hay otra observación clave relacionada con ‘ (1/n!)(1/n!) viene después.

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

Ya tenemos una interpretación para 0 en el mundo tipo: 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 f es una función tipo, ¿cómo se ve f(0) ? Bueno, ciertamente no tenemos acceso a nada de tipo 0 , por lo que las construcciones de f(x) que requieren una x no están disponibles. Lo que queda son esos 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 functor Maybe , 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 valor None . Para una lista, de manera similar, obtenemos solo el término correspondiente a la lista vacía.

Cuando lo traemos de vuelta 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 cualquier x ) se pueden obtener sin acceso a una x : eso es , la cantidad de términos ‘vacíos’.

Uniéndolo: completa la interpretación de una serie de Maclaurin

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

Si consideramos, sin embargo, el tipo f⁽ⁿ⁾(0) a la luz de lo anterior, vemos que se puede interpretar como el tipo de contextos n place para un término de tipo f(x) que ya no contiene una x – es decir, cuando las “integramos” n veces, 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 contextos n place vacíos hay. ¡Estamos casi allí!

Pero, ¿dónde termina (1/n!) ? El examen del proceso de tipo ‘diferenciación’ nos muestra que, cuando se aplica varias veces, conserva el ‘orden’ en el que se extraen los subtítulos. Por ejemplo, considere el término (x₀, x₁) de tipo x × x y 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 vienen del mismo término, porque hay 2! = 2 2! = 2 formas de tomar dos elementos de dos, preservando el orden. En general, hay n! formas de tomar n elementos de n . Entonces, para contar el número de configuraciones de un tipo de functor que tienen n elementos, tenemos que contar el tipo f⁽ⁿ⁾(0) y dividir por n! , exactamente como en los coeficientes de la serie Maclaurin.

Entonces dividiendo por n! resulta ser interpretable simplemente como sí mismo.

Pensamientos finales: definiciones “recursivas” y analítica

Primero, algunas observaciones:

  • si una función f: ℝ → ℝ tiene una derivada, esta derivada es única
  • Del mismo modo, 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 derivados 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 tipos recursivas. 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 en la serie de Maclaurin.

Pero como confiamos en que estas expresiones son estrictamente ‘diferenciables’, aunque 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 funciones ℝ → ℝ, sabemos que, si estamos 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 más riguroso.

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

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

Ahora, sin duda, esta es solo una forma de averiguar qué está pasando aquí y probablemente haya muchas otras maneras.

Resumen: TL; DR

  • tipo ‘diferenciación’ corresponde a ‘ hacer un agujero ‘.
  • aplicar un functor a 0 nos da los términos ‘vacíos’ para ese functor.
  • Por lo tanto, las series de poder de Maclaurin (algo) corresponden rigurosamente a la enumeración de la cantidad de miembros de un tipo de functor con un cierto número de elementos.
  • la diferenciación implícita lo hace más estanco.
  • la singularidad de los derivados y la unicidad de las series de potencias significa que podemos cambiar los detalles y funciona.

Teoría de tipos dependientes y funciones de tipo ‘arbitrarias’

Mi primera respuesta a esta pregunta fue alta en conceptos y baja en detalles y reflejada en la subversión, ‘¿qué está pasando?’; esta respuesta será la misma pero se enfocará en la subversión, ‘¿podemos obtener funciones de tipo arbitrarias?’.

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

Entonces la sum

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

podría estar escrito

 Σ[i ∈ ℕ]aᵢXⁱ 

donde a es una secuencia de números reales, por ejemplo. El producto se representaría de manera similar con Π 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 esto un candidato para una representación en una teoría de tipos? ¡Seguro!

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

Curry-Howard y tipos dependientes

El ‘isomorfismo de Curry-Howard’ comenzó como una observación de que los términos y las reglas del tipo de cálculo lambda simplemente tipificado corresponden exactamente a la deducción natural (formulada por Gentzen) aplicada a la lógica proposicional intuicionista, con tipos que toman el lugar de las proposiciones , y los términos toman el lugar de 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 teóricos de tipo. Una de las cosas más obvias a considerar es si, y cómo, esta correspondencia para la lógica proposicional se puede extender a lógicas predicativas o de orden superior. Las teorías de tipo dependiente surgieron inicialmente de esta avenida de exploración.

Para una introducción al isomorfismo de Curry-Howard para el cálculo de lambda simplemente tipado, ver aquí . Como ejemplo, si queremos demostrar A ∧ B , debemos probar A y demostrar 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 simplemente tipado:

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

Existen correspondencias similares para y tipos de sum, y tipos de funciones, y las diversas reglas de eliminación.

Una proposición no demostrable (intuicionísticamente 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 de tipos. Hay muchas maneras en que esto se ha formalizado (ver esta introducción a la Teoría del Tipo Intuicionista 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 los términos de las proposiciones. Si permitimos que las expresiones de tipo contengan términos, entonces un tratamiento en el estilo de cálculo lambda se presenta inmediatamente como una posibilidad.

Teniendo en cuenta solo las pruebas constructivas, ¿qué constituye una prueba de ∀x ∈ XP(x) ? Podemos considerarlo como una función de prueba, tomando términos ( x ) para las pruebas de sus proposiciones correspondientes ( P(x) ). So members (proofs) of the type (proposition) ∀x : XP(x) are ‘dependent functions’, which for each x in X give a term of type P(x) .

What about ∃x ∈ XP(x) ? We need any member of X , x , together with a proof of P(x) . So members (proofs) of the type (proposition) ∃x : XP(x) are ‘dependent pairs’: a distinguished term x in X , together with a term of type P(x) .

Notation: I will use

 ∀x ∈ X... 

for actual statements about members of the class X , and

 ∀x : X... 

for type expressions corresponding to universal quantification over type X . Likewise for .

Combinatorial considerations: products and sums

As well as the Curry-Howard correspondence of types with propositions, we have the combinatorial correspondence of algebraic types with numbers and functions, which is the main point of this question. Happily, this can be extended to the dependent types outlined above!

I will use the modulus notation

 |A| 

to represent the ‘size’ of a type A , to make explicit the correspondence outlined in the question, between types and numbers. Note that this is a concept outside of the theory; I do not claim that there need be any such operator within the language.

Let us count the possible (fully reduced, canonical) members of type

 ∀x : XP(x) 

which is the type of dependent functions taking terms x of type X to terms of type P(x) . Each such function must have an output for every term of X , and this output must be of a particular type. For each x in X , then, this gives |P(x)| ‘choices’ of output.

The punchline is

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

which of course doesn’t make huge deal of sense if X is IO () , but is applicable to algebraic types.

Similarly, a term of type

 ∃x : XP(x) 

is the type of pairs (x, p) with p : P(x) , so given any x in X we can construct an appropriate pair with any member of P(x) , giving |P(x)| ‘choices’.

Por lo tanto,

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

with the same caveats.

This justifies the common notation for dependent types in theories using the symbols Π and Σ , and indeed many theories blur the distinction between ‘for all’ and ‘product’ and between ‘there is’ and ‘sum’, due to the above-mentioned correspondences.

We are getting close!

Vectors: representing dependent tuples

Can we now encode numerical expressions like

 Σ[n ∈ ℕ]Xⁿ 

as type expressions?

No exactamente. While we can informally consider the meaning of expressions like Xⁿ in Haskell, where X is a type and n a natural number, it’s an abuse of notation; this is a type expression containing a number: distinctly not a valid expression.

On the other hand, with dependent types in the picture, types containing numbers is precisely the point; in fact, dependent tuples or ‘vectors’ are a very commonly-cited example of how dependent types can provide pragmatic type-level safety for operations like list access . A vector is just a list along with type-level information regarding its length: precisely what we are after for type expressions like Xⁿ .

For the duration of this answer, let

 Vec X n 

be the type of length- n vectors of X -type values.

Technically n here is, rather than an actual natural number, a representation in the system of a natural number. We can represent natural numbers ( Nat ) in Peano style as either zero ( 0 ) or the successor ( S ) of another natural number, and for n ∈ ℕ I write ˻n˼ to mean the term in Nat which represents n . For example, ˻3˼ is S (S (S 0)) .

Entonces nosotros tenemos

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

for any n ∈ ℕ .

Nat types: promoting ℕ terms to types

Now we can encode expressions like

 Σ[n ∈ ℕ]Xⁿ 

as types. This particular expression would give rise to a type which is of course isomorphic to the type of lists of X , as identified in the question. (Not only that, but from a category-theoretic point of view, the type function – which is a functor – taking X to the above type is naturally isomorphic to the List functor.)

One final piece of the puzzle for ‘arbitrary’ functions is how to encode, for

 f : ℕ → ℕ 

expressions like

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

so that we can apply arbitrary coefficients to a power series.

We already understand the correspondence of algebraic types with numbers, allowing us to map from types to numbers and type functions to numerical functions. We can also go the other way! – taking a natural number, there is obviously a definable algebraic type with that many term members, whether or not we have dependent types. We can easily prove this outside of the type theory by induction. What we need is a way to map from natural numbers to types, inside the system.

A pleasing realisation is that, once we have dependent types, proof by induction and construction by recursion become intimately similar – indeed they are the very same thing in many theories. Since we can prove by induction that types exist which fulfil our needs, should we not be able to construct them?

There are several ways to represent types at the term level. I will use here an imaginary Haskellish notation with * for the universe of types, itself usually considered a type in a dependent setting. 1

Likewise, there are also at least as many ways to notate ‘ -elimination’ as there are dependent type theories. I will use a Haskellish pattern-matching notation.

We need a mapping, α from Nat to * , with the property

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

The following pseudodefinition suffices.

 data Zero -- empty type data Successor a = Z | Suc a -- Successor ≅ Maybe α : Nat -> * α 0 = Zero α (S n) = Successor (α n) 

So we see that the action of α mirrors the behaviour of the successor S , making it a kind of homomorphism. Successor is a type function which ‘adds one’ to the number of members of a type; that is, |Successor a| = 1 + |a| for any a with a defined size.

For example α ˻4˼ (which is α (S (S (S (S 0)))) ), is

 Successor (Successor (Successor (Successor Zero))) 

and the terms of this type are

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

giving us exactly four elements: |α ˻4˼| = 4 .

Likewise, for any n ∈ ℕ , we have

 |α ˻n˼| = n 

según sea necesario.

  1. Many theories require that the members of * are mere representatives of types, and an operation is provided as an explicit mapping from terms of type * to their associated types. Other theories permit the literal types themselves to be term-level entities.

‘Arbitrary’ functions?

Now we have the apparatus to express a fully general power series as a type!

The series

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

becomes the type

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

where ˻f˼ : Nat → Nat is some suitable representation within the language of the function f . We can see this as follows.

 |∃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) 

Just how ‘arbitrary’ is this? We are limited not only to integer coefficients by this method, but to natural numbers. Apart from that, f can be anything at all, given a Turing Complete language with dependent types, we can represent any analytic function with natural number coefficients.

I haven’t investigated the interaction of this with, for example, the case provided in the question of List X ≅ 1/(1 - X) or what possible sense such negative and non-integer ‘types’ might have in this context.

Hopefully this answer goes some way to exploring how far we can go with arbitrary type functions.