haskell - tag - ¿Por qué necesitamos contenedores?

google tag manager

Question

(Como excusa: el título imita el título de ¿Por qué necesitamos mónadas? )

Hay containers (y indexed ) (y hasochistic ) y descriptions . Pero los contenedores son problematic y para mi experiencia muy pequeña es más difícil pensar en términos de contenedores que en términos de descripciones. El tipo de contenedores no indexados es isomorfo a Σ - eso es demasiado inespecífico. La descripción de formas y posiciones ayuda, pero en

⟦_⟧ᶜ : ∀ {α β γ} -> Container α β -> Set γ -> Set (α ⊔ β ⊔ γ)
⟦ Sh ◃ Pos ⟧ᶜ A = ∃ λ sh -> Pos sh -> A
Kᶜ : ∀ {α β} -> Set α -> Container α β
Kᶜ A = A ◃ const (Lift ⊥)

estamos esencialmente usando Σ lugar de formas y posiciones.

El tipo de mónadas libres estrictamente positivas sobre contenedores tiene una definición bastante directa, pero el tipo de mónadas Freer me parece más simple (y en cierto sentido las mónadas Freer son incluso mejores que las mónadas Free habituales, como se describe en el paper ).

Entonces, ¿qué podemos hacer con los contenedores de una manera más agradable que con descripciones u otra cosa?

Answer 1

En mi opinión, el valor de los contenedores (como en la teoría de contenedores) es su uniformidad . Esa uniformidad ofrece un margen considerable para utilizar representaciones de contenedores como base para las especificaciones ejecutables, y quizás incluso para la derivación de programas asistidos por máquinas.

Contenedores: una herramienta teórica, no una buena estrategia de representación de datos en tiempo de ejecución

No recomendaría puntos de referencia de contenedores (normalizados) como una buena forma de propósito general para implementar estructuras de datos recursivas. Es decir, es útil saber que un funtor dado tiene (hasta iso) una presentación como contenedor, porque te dice que la funcionalidad del contenedor genérico (que se implementa fácilmente, de una vez por todas, gracias a la uniformidad) se puede instanciar a su functor particular, y qué comportamiento debe esperar. Pero eso no quiere decir que la implementación de un contenedor sea eficiente de ninguna manera práctica. De hecho, generalmente prefiero codificaciones de primer orden (etiquetas y tuplas, en lugar de funciones) de datos de primer orden.

Para corregir la terminología, digamos que el tipo Cont de contenedores (en Set , pero hay otras categorías disponibles) está dado por un constructor <| embalando dos campos, formas y posiciones

S : Set
P : S -> Set

(Esta es la misma firma de datos que se utiliza para determinar un tipo Sigma, o un tipo Pi, o un tipo W, pero eso no significa que los contenedores sean iguales a cualquiera de estas cosas, o que estas cosas sean las mismas como el uno al otro.)

La interpretación de tal cosa como functor está dada por

[_]C : Cont -> Set -> Set
[ S <| P ]C X = Sg S / s -> P s -> X -- I''d prefer (s : S) * (P s -> X)
mapC : (C : Cont){X Y : Set} -> (X -> Y) -> [ C ]C X -> [ C ]C Y
mapC (S <| P) f (s , k) = (s , f o k) -- o is composition

Y ya estamos ganando Ese es el map implementado de una vez por todas. Lo que es más, las leyes de funtores se mantienen solo por computación. No es necesario recurrir a la estructura de tipos para construir la operación o para probar las leyes.

Las descripciones son contenedores desnormalizados

Nadie intenta afirmar que, desde el punto de vista operativo, Nat <| Fin Nat <| Fin ofrece una implementación eficiente de listas, solo que al hacer esa identificación aprendemos algo útil sobre la estructura de las listas.

Déjame decir algo sobre las descripciones . Para el beneficio de los lectores perezosos, permítanme reconstruirlos.

data Desc : Set1 where
var : Desc
sg pi : (A : Set)(D : A -> Desc) -> Desc
one : Desc -- could be Pi with A = Zero
_*_ : Desc -> Desc -> Desc -- could be Pi with A = Bool
con : Set -> Desc -- constant descriptions as singleton tuples
con A = sg A / _ -> one
_+_ : Desc -> Desc -> Desc -- disjoint sums by pairing with a tag
S + T = sg Two / { true -> S ; false -> T }

Los valores en Desc describen los funtores cuyos puntos de fijación dan los tipos de datos. ¿Qué funtores describen?

[_]D : Desc -> Set -> Set
[ var ]D X = X
[ sg A D ]D X = Sg A / a -> [ D a ]D X
[ pi A D ]D X = (a : A) -> [ D a ]D X
[ one ]D X = One
[ D * D'' ]D X = Sg ([ D ]D X) / _ -> [ D'' ]D X
mapD : (D : Desc){X Y : Set} -> (X -> Y) -> [ D ]D X -> [ D ]D Y
mapD var f x = f x
mapD (sg A D) f (a , d) = (a , mapD (D a) f d)
mapD (pi A D) f g = / a -> mapD (D a) f (g a)
mapD one f <> = <>
mapD (D * D'') f (d , d'') = (mapD D f d , mapD D'' f d'')

Inevitablemente tenemos que trabajar por recursión sobre descripciones, por lo que es un trabajo más difícil. Las leyes de fideicomiso, también, no vienen gratis. Obtenemos una mejor representación de los datos, operacionalmente, porque no necesitamos recurrir a codificaciones funcionales cuando las tuplas concretas lo hagan. Pero tenemos que trabajar más duro para escribir programas.

Tenga en cuenta que cada contenedor tiene una descripción:

sg S / s -> pi (P s) / _ -> var

Pero también es cierto que cada descripción tiene una presentación como un contenedor isomorfo.

ShD : Desc -> Set
ShD D = [ D ]D One
PosD : (D : Desc) -> ShD D -> Set
PosD var <> = One
PosD (sg A D) (a , d) = PosD (D a) d
PosD (pi A D) f = Sg A / a -> PosD (D a) (f a)
PosD one <> = Zero
PosD (D * D'') (d , d'') = PosD D d + PosD D'' d''
ContD : Desc -> Cont
ContD D = ShD D <| PosD D

Es decir, los contenedores son una forma normal de descripciones. Es un ejercicio para demostrar que [ D ]DX es naturalmente isomorfo a [ ContD D ]CX . Eso hace la vida más fácil, porque para decir qué hacer para las descripciones, es suficiente en principio decir qué hacer para sus formas normales, los contenedores. La operación anterior de mapD podría, en principio, obtenerse fusionando los isomorfismos a la definición uniforme de mapC .

Estructura diferencial: los contenedores muestran el camino

Del mismo modo, si tenemos una noción de igualdad, podemos decir qué contextos de un agujero son para contenedores de manera uniforme

_-[_] : (X : Set) -> X -> Set
X -[ x ] = Sg X / x'' -> (x == x'') -> Zero
dC : Cont -> Cont
dC (S <| P) = (Sg S P) <| (/ { (s , p) -> P s -[ p ] })

Es decir, la forma de un contexto de un agujero en un contenedor es el par de la forma del contenedor original y la posición del agujero; las posiciones son las posiciones originales aparte de la del hoyo. Esa es la versión relevante para la prueba de "multiplicar por el índice, disminuir el índice" al diferenciar series de potencias.

Este tratamiento uniforme nos da la especificación de la cual podemos derivar el programa centenario para calcular la derivada de un polinomio.

dD : Desc -> Desc
dD var = one
dD (sg A D) = sg A / a -> dD (D a)
dD (pi A D) = sg A / a -> (pi (A -[ a ]) / { (a'' , _) -> D a'' }) * dD (D a)
dD one = con Zero
dD (D * D'') = (dD D * D'') + (D * dD D'')

¿Cómo puedo verificar que mi operador derivado para las descripciones sea correcto? ¡Al marcarlo contra la derivada de los contenedores!

No caiga en la trampa de pensar que solo porque una presentación de alguna idea no es útil operativamente no puede ser conceptualmente útil.

En mónadas "Freer"

Una última cosa. El truco de Freer equivale a reorganizar un funtor arbitrario de una manera particular (cambiando a Haskell)

data Obfuncscate f x where
(:<) :: forall p. f p -> (p -> x) -> Obfuncscate f x

pero esta no es una alternativa a los contenedores. Este es un ligero currying de una presentación de contenedor. Si tuviéramos fuertes existenciales y tipos dependientes, podríamos escribir

data Obfuncscate f x where
(:<) :: pi (s :: exists p. f p) -> (fst s -> x) -> Obfuncscate f x

de modo que (exists p. fp) represente formas (donde puede elegir su representación de posiciones, luego marque cada lugar con su posición), y fst selecciona el testigo existencial de una forma (la representación de posición que elija). Tiene el mérito de ser obviamente estrictamente positivo exactamente porque es una presentación de contenedor.

En Haskell, por supuesto, tienes que deducir lo existencial, lo que afortunadamente deja una dependencia solo en la proyección del tipo. Es la debilidad de lo existencial lo que justifica la equivalencia de Obfuncscate f y f . Si prueba el mismo truco en una teoría de tipos dependientes con fuertes existenciales, la codificación pierde su singularidad porque puede proyectar y distinguir diferentes opciones de representación para las posiciones. Es decir, puedo representar a Just 3 por

Just () :< const 3

o por

Just True :< / b -> if b then 3 else 5

y en Coq, digamos, estos son provablemente distintos.

Desafío: caracterizar funciones polimórficas

Cada función polimórfica entre tipos de contenedores se da de una manera particular. Está esa uniformidad trabajando para aclarar nuestra comprensión nuevamente.

Si tienes algo

f : {X : Set} -> [ S <| T ]C X -> [ S'' <| T'' ]C X

está (extensionalmente) dado por los siguientes datos, que no mencionan ningún elemento:

toS : S -> S''
fromP : (s : S) -> P'' (toS s) -> P s
f (s , k) = (toS s , k o fromP s)

Es decir, la única forma de definir una función polimórfica entre contenedores es decir cómo traducir las formas de entrada a las formas de salida, y luego decir cómo llenar las posiciones de salida desde las posiciones de entrada.

Para su representación preferida de functors estrictamente positivos, proporcione una caracterización similarmente ajustada de las funciones polimórficas que elimine la abstracción sobre el tipo de elemento. (Para las descripciones, usaría exactamente su capacidad de redirección para los contenedores).

Desafío: capturar la "transposibilidad"

Dado dos functors, f y g , es fácil decir cuál es su composición de fog : (fog) x envuelve cosas en f (gx) , dándonos " f -estructuras de g -estructuras". Pero, ¿se puede imponer fácilmente la condición adicional de que todas las estructuras g almacenadas en la estructura f tengan la misma forma?

Digamos que f >< g captura el fragmento transponible de fog , donde todas las formas g son iguales, de modo que podemos convertir la cosa en una estructura g estructuras f . Por ejemplo, mientras [] o [] da listas irregulares de listas, [] >< [] da matrices rectangulares ; [] >< Maybe da listas que son todas Nothing o todas Just .

Give >< para su representación preferida de funtores estrictamente positivos. Para contenedores, es así de fácil.

(S <| P) >< (S'' <| P'') = (S * S'') <| / { (s , s'') -> P s * P'' s'' }

Conclusión

Los contenedores, en su forma normalizada Sigma-then-Pi, no están destinados a ser una representación de datos eficiente de la máquina. Pero el conocimiento de que un functor dado, implementado sin embargo, tiene una presentación como un contenedor nos ayuda a comprender su estructura y darle un equipo útil. Muchas construcciones útiles se pueden dar abstractamente para contenedores, de una vez por todas, cuando se deben dar caso por caso para otras presentaciones. Por lo tanto, sí, es una buena idea aprender sobre contenedores, aunque solo sea para comprender la razón de ser de las construcciones más específicas que realmente implementa.