haskell añadir - Abusar del álgebra de los tipos de datos algebraicos:¿por qué funciona esto?




elementos una (7)

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

Habiendo definido los tipos básicos.

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

y utilizando la abreviatura para X•X y 2X para X+X etcétera, podemos definir expresiones algebraicas para, por ejemplo, listas enlazadas

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 volverse loco con estas expresiones, y tratar de resolver para L y T Podría hacer esto a través de 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 enlazada:

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 potencias 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 (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 algebraico?) Pero conducen a resultados sensatos. ¿El cociente de dos tipos de datos algebraicos tiene algún significado en ciencias de la computación, o es solo un engaño 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 tipos, o los tipos requieren una representación de series de potencias? Si puede definir una clase de funciones, ¿tiene algún significado la composición de funciones?


Answers

Descargo de responsabilidad: mucho de esto realmente no funciona del todo bien cuando contabiliza ⊥, así que voy a ignorarlo descaradamente por simplicidad.

Algunos puntos iniciales:

  • Tenga en cuenta que "unión" probablemente no sea el mejor término para A + B aquí, ya que es específicamente una unión desunida 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 de 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. No hay uno estándar, pero el nombre más común es 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 habrá notado, Haskell tiende a tomar prestados conceptos de la teoría de categorías, y todo lo anterior tiene una interpretación muy sencilla como tal:

  • Dados los objetos A y B en Hask , su producto A × B es el tipo único (hasta isomorfismo) que permite dos proyecciones fst : A × B → A y snd : A × B → B, donde se proporciona cualquier tipo C y funciones f : C → A, g : C → B puede definir el emparejamiento f && g : C → A × B de tal manera que fst ∘ (f &&& g) = f y lo mismo para g . La parametridad garantiza las propiedades universales automáticamente y mi elección menos sutil de nombres debería darte una 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 asigna cualquier tipo C y funciones f : A → C, g : B → C, puede define la copairing f ||| g : A + B → C tal que las equivalencias obvias se mantienen. Una vez más, 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 la función de copairing es either .

Muchas de las propiedades de los tipos de producto y suma pueden derivarse de lo anterior. Tenga en cuenta que cualquier tipo de 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 flechas de la categoría. Nuestras flechas son funciones, nuestros objetos son tipos con tipo * y el tipo A -> B comporta como B A en el contexto de la manipulación algebraica de tipos. Si no es obvio por qué debería ser así, 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) . Para Maybe Bool -> A tenemos 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é se justifica su uso de la expansión de series 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 Demostrar el comportamiento algebraico. Para hacer explícita esa perspectiva:

  • 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 suma Either AB representa un valor de A o B , con las ramas izquierda y derecha distinguidas. Como se mencionó anteriormente, esta es una unión desunida, y el número de habitantes del tipo de suma es la suma del número de habitantes de los sumandos.

  • 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 estos mapas 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, en realidad no funciona muy bien en este contexto: tenemos una unión separada en lugar de la unión estándar de conjuntos, no hay una interpretación obvia de intersección o muchas otras operaciones de conjunto, y por lo general, no se preocupa por establecer una membresía (dejándolo en el comprobador de tipos)

Por otro lado, las construcciones anteriores dedican mucho tiempo a hablar sobre el conteo de 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 a través de generando funciones , luego hace lo mismo para "secuencias" que son idénticas a las listas de Haskell usando exactamente la misma técnica que hiciste.

Edit: Ah, y aquí hay un bono rápido que creo que demuestra el punto de manera sorprendente. Mencionó en un comentario que para un tipo de árbol T = 1 + T^2 puede derivar la identidad T^6 = 1 , que es claramente errónea. Sin embargo, T^7 = T se mantiene, y se puede construir directamente una bijección entre árboles y siete tuplas de árboles, cf. Los siete árboles en uno de Andreas Blass .

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


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


Los árboles binarios se definen mediante 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 semiring 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 la semired de números complejos usualmente 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 semirings. Pero a menudo podemos eliminar las restas de nuestros argumentos si tenemos una regla que nos permita 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 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 potencias (en el anillo de las series de potencias formales) se pueden transferir 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) al mostrar que dos series de potencias son iguales. Pero también puede deducir información sobre los tipos inspeccionando los términos en la serie de potencias. No estoy seguro de lo que debería ser la declaración formal aquí. (Recomiendo el artículo de Brent Yorgey sobre especies combinatorias para algunos trabajos que están estrechamente relacionados, pero las especies no son lo mismo que los tipos).

Lo que encuentro totalmente alucinante es que lo que has descubierto puede extenderse al cálculo. Los teoremas sobre el cálculo se pueden transferir a la semiringura de tipos. De hecho, incluso los argumentos sobre diferencias finitas pueden transferirse y se encuentra que los teoremas clásicos del análisis numérico tienen interpretaciones en la teoría de tipos.

¡Que te diviertas!



Teoría de tipos dependiente y funciones de tipo 'arbitrario'

Mi primera respuesta a esta pregunta fue alta en conceptos y baja en detalles y reflejada en la pregunta secundaria, '¿qué está pasando?'; esta respuesta será la misma pero enfocada en la pregunta secundaria, '¿podemos obtener funciones de tipo arbitrario?'.

Una extensión de las operaciones algebraicas de suma y producto son los llamados 'grandes operadores', 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 la notación de Sigma .

Entonces la suma

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 a 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 tipo que tienen representaciones inmediatas de estas expresiones es la clase de teorías de tipo "dependientes": teorías con tipos dependientes. Naturalmente, tenemos términos que dependen de los términos y en lenguajes como Haskell con funciones de tipo y cuantificación de tipo, términos y tipos según los tipos. En una configuración dependiente, también tenemos tipos dependiendo de los términos. Haskell no es un lenguaje tipificado de forma 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ó su vida como una observación de que los términos y las reglas de evaluación de tipos del cálculo lambda de tipo simple corresponden exactamente a la deducción natural (según lo formula Gentzen) aplicada a la lógica proposicional intuicionista, con tipos que ocupan el lugar de las proposiciones. y los términos que 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 los teóricos del tipo. Una de las cosas más obvias a considerar es si, y cómo, esta correspondencia para la lógica proposicional puede extenderse al predicado o las lógicas de orden superior. Las teorías de tipo dependientes surgieron inicialmente de esta avenida de exploración.

Para una introducción al isomorfismo de Curry-Howard para el cálculo lambda de tipo simple, vea here . Como ejemplo, si queremos probar A ∧ B debemos probar A y 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 el cálculo lambda simplemente mecanografiado:

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

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

Una proposición no demostrable (intuicionista 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 formas en que esto se ha formalizado (consulte esta introducción a la Teoría de Tipos Intuicionistas 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, a function taking terms to propositions. Si permitimos que las expresiones tipográficas contengan términos, entonces un tratamiento en estilo de cálculo lambda se presenta inmediatamente como una posibilidad.

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

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

Notación: voy a utilizar

∀x ∈ X...

para las declaraciones reales sobre los miembros de la clase X, y

∀x : X...

para expresiones de tipo correspondientes a la cuantificación universal sobre tipo X. Igualmente para .

Consideraciones combinatorias: productos y sumas.

Además de la correspondencia de 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 del módulo

|A|

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

Contemos los posibles miembros (completamente reducidos, canónicos) de tipo

∀x : X.P(x)

que es el tipo de funciones dependientes que llevan los términos xde tipo Xa los términos de tipo P(x). Cada una de estas 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 punchline es

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

que por supuesto no tiene mucho sentido si 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), por lo que, dado que xen cualquiera Xpodemos construir un par apropiado con cualquier miembro de P(x), dando |P(x)|"elecciones"

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 difuminan la distinción entre "para todos" y "producto" y entre "existe" 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 de manera informal el significado de expresiones como Xⁿen Haskell, donde Xes un tipo y nun número natural, es un abuso de notación; esta es una expresión de tipo que contiene un número: claramente no es una expresión válida.

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

Para la duración de esta respuesta, vamos a

Vec X n

Ser el tipo de nvectores de longitud 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 los 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˼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 X, como se identifica en la pregunta. (No solo eso, sino que desde un punto de vista teórico de la categoría, la función de tipo, que es un functor, llevar Xal tipo anterior es naturalmente isomorfa al 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 asignar de tipos a números y funciones de tipo a funciones numéricas. ¡También podemos ir por el otro lado! - tomando un número natural, obviamente hay un tipo algebraico definible con tantos miembros del término, tengamos o no tipos dependientes. Fácilmente podemos probar esto fuera de la teoría de tipos por inducción. Lo que necesitamos es una forma de mapear desde números naturales a tipos, dentro del sistema.

Una conclusión agradable es que, una vez que tenemos tipos dependientes, la prueba por inducción y la construcción por recursión se vuelven íntimamente similares, de hecho, son lo mismo en muchas teorías. Ya que 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 en el nivel de término. Usaré aquí una notación Haskellish imaginaria *para el universo de tipos, que en general se considera un tipo en una configuración dependiente. 1

Del mismo modo, también hay al menos tantas formas de anotar ' -eliminación' como teorías de tipo dependientes. Usaré una notación de coincidencia de patrones de Haskellish.

Necesitamos un mapeo, αde Nata *, 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)

Así que vemos que la acción de αrefleja el comportamiento del sucesor S, convirtiéndolo en un tipo 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.

Igualmente, para cualquiera n ∈ ℕ, tenemos

|α ˻n˼| = n

según sea necesario.

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

¿Funciones 'arbitrarias'?

¡Ahora tenemos el aparato para expresar una serie de potencia totalmente general 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 de 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 de números naturales.

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

Esperemos que esta respuesta sirva para explorar en qué medida podemos llegar con funciones de tipo arbitrarias.


El Álgebra de los procesos de comunicación (ACP) trata con tipos similares de expresiones para procesos. Ofrece sumas y multiplicaciones como operadores para elección y secuencia, con elementos neutros asociados. Sobre la base de 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 los lenguajes de programación con ACP. El pasado abril presenté un trabajo de investigación en Scala Days 2012, disponible en http://code.google.com/p/subscript/

En la conferencia mostré un depurador ejecutando 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 símbolo comercial 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; Vea el artículo de Wikipedia. Me pregunto para qué sería la analogía de la bolsa.

L = 1 / (1-X)

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

searchCommand = pulsado (searchButton) + tecla (Enter)

cancelCommand = pulsado (cancelButton) + tecla (Escape)

se puede escribir de manera más concisa al hacer que los dos refinamientos "clic" y "clave" sean implícitos (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 se 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í datos como compañeros; así acuño el término "álgebra de ítems".


def dump(fname,iterable):
  with open(fname,'w') as f:
    reduce(lambda x, y: f.write(unicode(y,'utf-8')), iterable)




haskell functional-programming ocaml algebraic-data-types miranda